Coquand's calculus of constructions: A mathematical foundation for a proof development system

Research paper by Jonathan P. Seldin

Indexed on: 01 Sep '92Published on: 01 Sep '92Published in: Formal Aspects of Computing


The calculus of constructions of Coquand, which is a version of higher order typedλ-calculus based on the dependent function type, is considered from the perspective of its use as the mathematical foundation for a proof development system. The paper considers formulations of the calculus, the underlying consistency of the formalism (i.e., the strong normalisation theorem), and the proof theory of adding assumptions for notions from logic and set theory. Proofs are not given, but references to them are.