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

DOI10.1007/BF01211392zbMath0766.03007OpenAlexW2012195956MaRDI QIDQ1201296

Jonathan P. Seldin

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

zbMATH Keywords

calculus of constructionsnormalisationconsistency of assumptionshigher order typed \(\lambda\)-calculusproof development system

Mathematics Subject Classification ID

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)

Interpreting HOL in the calculus of constructions ⋮ Variants of the basic calculus of constructions ⋮ On the proof theory of Coquand's calculus of constructions ⋮ A Gentzen-style sequent calculus of constructions with expansion rules ⋮ Type Theories from Barendregt’s Cube for Theorem Provers

Uses Software

• Nuprl

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