Semantic foundations for embedding HOL in Nuprl

1. Part IIIA: SCI Coherence Overview, 1995. Unapproved draft IEEE-P1596–05Nov90-doc197-iii.

   Google Scholar 

2. Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science. Springer, 1995.

   Google Scholar 

3. S. F. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, 1987.

   Google Scholar 

4. V. Breazu-Tannen and R. Subrahmanyam. Logical and computational aspects of programming with sets/bags/lists. In Automata, Languages and Programming: 18 ^th International Colloquium, Lecture Notes in Computer Science, pages 60–75. Springer-Verlag, 1991.

   Google Scholar 

5. R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.

   Google Scholar 

6. P. Dybjer. Inductive sets and families in Martin-Löf's type theory and their settheoretic semantics. In Proceedings of the B.R.A. Workshop on Logical Frameworks, Sophia-Antipolis, France, June 1990.

   Google Scholar 

7. A. Gordon. Functional Programming and Input/Output. Cambrige University Press, 1994.

   Google Scholar 

8. M. J. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

   Google Scholar 

9. M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, UK, 1993.

   Google Scholar 

10. D. J. Howe. Equality in lazy computation systems. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 198–203. IEEE Computer Society, June 1989.

    Google Scholar 

11. D. J. Howe. On computational open-endedness in Martin-Löf's type theory. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science, pages 162–172. IEEE Computer Society, 1991.

    Google Scholar 

12. D. J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 1996. To appear.

    Google Scholar 

13. D. J. Howe and S. D. Stoller. An operational approach to combining classical set theory and functional programming languages. In Theoretical Aspects of Computer Software, Lecture Notes in Computer Science. Springer-Verlag, 1994.

    Google Scholar 

14. P. B. Jackson. Exploring abstract algebra in constructive type theory. In A. Bundy, editor, 12th Conference on Automated Deduction, Lecture Notes in Artifical Intelligence. Springer, June 1994.

    Google Scholar 

15. B. Jacobs and T. Melham. Translating dependent type theory into higher order logic. In Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 209–229. Springer, 1993.

    Google Scholar 

16. P. Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153–175, Amsterdam, 1982. North Holland.

    Google Scholar 

17. T. Melham. The HOL logic extended with quantification over type variables. Formal Methods in System Design, 3(1–2):7–24, August 1993.

    Google Scholar 

18. R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.

    Google Scholar 

19. E. Ritter and A. Pitts. A fully abstract translation between a λ-calculus with reference types and Standard ML. In Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 397–413. Springer, 1995.

    Google Scholar 

20. M. van der Voort. Introducing well-founded function definitions in HOL. In Higher Order Logic Theorem Proving and Its Applications, volume A-20 of IFIP Transactions, pages 117–131. North-Holland, 1993.

    Google Scholar 

Download references