Proof Terms for Simply Typed Higher Order Logic
- 1 January 2000
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 10 references indexed in Scilit:
- Unification and anti-unification in the calculus of constructionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Efficient representation and validation of proofsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Proof-carrying codePublished by Association for Computing Machinery (ACM) ,1997
- Unification of higher-order patterns in linear time and spaceJournal of Logic and Computation, 1996
- IsabellePublished by Springer Nature ,1994
- Functional unification of higher-order patternsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1993
- Logic programming in the LF logical frameworkPublished by Cambridge University Press (CUP) ,1991
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple UnificationJournal of Logic and Computation, 1991
- The foundation of a generic theorem proverJournal of Automated Reasoning, 1989
- Seventy-five problems for testing automatic theorem proversJournal of Automated Reasoning, 1986