No CrossRef data available.
Article contents
Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions
Published online by Cambridge University Press: 04 March 2009
Abstract
We present an algebraic approach to the syntax and semantics of Martin-Löf type theory and the calculus of constructions developed by T. Coquand and G. Huet. In our approach, models of this theory and this calculus are treated as three-sorted partial algebras, called ITSΠ-structures, described by essentially algebraic theories. We give a proof that derived statements of Martin-Löf type theory hold in appropriate ITSΠ-structures. In this proof, a formal translation from the language of terms and types into the language of terms of an appropriate essentially algebraic theory of ITSΠ-structures is used. A straightforward set-theoretic construction of ITSΠ-structures that are models of Martin-Löf type theory is demonstrated. We present a construction of a recursive ITSΠ-structure (i.e. its partial and total operations are recursive functions over some alphabet) that is a model of the calculus of constructions and demonstrates the decidability of this calculus.
- Type
- Research Article
- Information
- Copyright
- Copyright © Cambridge University Press 1993