Paper: Encoding the calculus of constructions in a higher-order logic (at LICS 1993)

Authors: Amy Felty

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 λ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

BibTeX

  @InProceedings{Felty-Encodingthecalculus,
    author = 	 {Amy Felty},
    title = 	 {Encoding the calculus of constructions in a higher-order logic},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)},
    year =	 {1993},
    month =	 {June}, 
    pages =      {233--244},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }