Proof Terms for Simply Typed Higher Order Logic

1. H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 118–309. Oxford University Press, 1992.

   Google Scholar 

2. B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.-C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, H. Laulhère, C. Muñoz, C. Murthy, C. Parent-Vigouroux, P. Loiseleur, C. Paulin-Mohring, A. Saïbi, and B. Werner. The Coq proof assistant reference manual — version 6.3.1. Technical report, INRIA, 1999.

   Google Scholar 

3. M. J. C. Gordon, J. M. J. Herbert, R. W. S. Hale, J. Harrison, W. Wong, and J. von Wright. Self-checking prover study — final report. Technical report, SRI, 1995. Available at http://www.csl.sri.com/reports/postscript/proofchecker.ps.gz.

4. D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.

   Article  MATH  Google Scholar 

5. G. C. Necula. Proof-carrying code. In Conference Record of POPL’ 97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106–119. ACM Press, New York, 1997.

   Chapter  Google Scholar 

6. G. C. Necula and P. Lee. Efficient representation and validation of proofs. In 13th IEEE Symp. Logic in Computer Science (LICS’98), pages 93–104. IEEE Computer Society Press, 1998.

   Google Scholar 

7. T. Nipkow. Functional unification of higher-order patterns. In 8th IEEE Symp. Logic in Computer Science, pages 64–74. IEEE Computer Society Press, 1993.

   Google Scholar 

8. L. C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–397, 1989.

   Article  MATH  Google Scholar 

9. L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer, 1994.

   MATH  Google Scholar 

10. F. J. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2:191–216, 1986.

    Article  MATH  Google Scholar 

11. F. Pfenning. Logic programming in the LF Logical Framework. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 66–78. Cambridge University Press, 1991.

    Google Scholar 

12. F. Pfenning. Unification and anti-unification in the calculus of constructions. In 6th IEEE Symposium on Logic in Computer Science, pages 74–85. IEEE Computer Society Press, 1991.

    Google Scholar 

13. Z. Qian. Unification of higher-order patterns in linear time and space. Journal of Logic and Computation, 6:315–341, 1996.

    Article  MATH  Google Scholar 

14. W. Wong. Recording and checking HOL proofs. In E. Schubert, P. Windley, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications. 8th International Workshop, volume 971 of LNCS, pages 353–68. Springer-Verlag, Berlin, 1995.

    Google Scholar 

Download references