Coquand's calculus of constructions: A mathematical foundation for a proof development system
DOI10.1007/BF01211392zbMath0766.03007OpenAlexW2012195956MaRDI QIDQ1201296
Publication date: 17 January 1993
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf01211392
calculus of constructionsnormalisationconsistency of assumptionshigher order typed \(\lambda\)-calculusproof development system
Theory of programming languages (68N15) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03) Combinatory logic and lambda calculus (03B40) Theory of computing (68Q99)
Related Items (5)
Uses Software
Cites Work
- Combinatory logic. With two sections by William Craig.
- The calculus of constructions
- A transfinite type theory with type variables
- Combinatory logic. Vol. II
- A sequent calculus for type assignment
- On the proof theory of Coquand's calculus of constructions
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Coquand's calculus of constructions: A mathematical foundation for a proof development system