Encoding the calculus of constructions in a higher-order logic
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 9, 233-244
- https://doi.org/10.1109/lics.1993.287584
Abstract
The author presents an encoding of the calculus of constructions (CC) in a higher-order intuitionistic logic (I) in a direct way, so that correct typing in CC corresponds to intuitionistic provability in a sequent calculus for I. In addition, she demonstrates a direct correspondence between proofs in these two systems. The logic I is an extension of hereditary Harrop formulas (hh), which serve as the logical foundation of the logic programming language lambda Prolog. Like hh, I has the uniform proof property, which allows a complete nondeterministic search procedure to be described in a straightforward manner. Via the encoding, this search procedure provides a goal directed description of proof checking and proof search in CC.Keywords
This publication has 6 references indexed in Scilit:
- Implementing tactics and tacticals in a higher-order logic programming languageJournal of Automated Reasoning, 1993
- Encoding dependent types in an intuitionistic logicPublished by Cambridge University Press (CUP) ,1991
- Introduction to generalized type systemsJournal of Functional Programming, 1991
- Uniform proofs as a foundation for logic programmingAnnals of Pure and Applied Logic, 1991
- The calculus of constructionsInformation and Computation, 1988
- A formulation of the simple theory of typesThe Journal of Symbolic Logic, 1940