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

DOI10.1007/BF01211392MaRDI QIDQ1201296zbMATH OpenOpenAlexFDO

Authors 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 constructionsconsistency of assumptionshigher order typed \(\lambda\)-calculusnormalisationproof development system

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Theory of programming languages (68N15) Theory of computing (68Q99)

Recommendations

• On the proof theory of Coquand's calculus of constructions
• The calculus of constructions
• scientific article; zbMATH DE number 4019061
• scientific article; zbMATH DE number 2182487
• scientific article; zbMATH DE number 4014064

Cites work

• A sequent calculus for type assignment
• A transfinite type theory with type variables
• Combinatory logic. Vol. II
• Combinatory logic. With two sections by William Craig.
• scientific article; zbMATH DE number 4191621 (Why is no real title available?)
• scientific article; zbMATH DE number 3657156 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3261581 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• scientific article; zbMATH DE number 3076631 (Why is no real title available?)
• On the proof theory of Coquand's calculus of constructions
• The calculus of constructions

Cited in

(15)

• The calculus of constructions
• A Gentzen-style sequent calculus of constructions with expansion rules
• The calculus of constructions as a framework for proof search with set variable instantiation
• Interpreting HOL in the calculus of constructions
• Variants of the basic calculus of constructions
• scientific article; zbMATH DE number 4014064 (Why is no real title available?)
• scientific article; zbMATH DE number 4019061 (Why is no real title available?)
• scientific article; zbMATH DE number 3928956 (Why is no real title available?)
• scientific article; zbMATH DE number 65528 (Why is no real title available?)
• scientific article; zbMATH DE number 1984518 (Why is no real title available?)
• A mechanized proof system of the third generation calculus in Coq
• Verified representations of Landau's ``Grundlagen in the \(\lambda\delta\) family and in the calculus of constructions
• Type theories from Barendregt's cube for theorem provers
• A modular construction of type theories
• On the proof theory of Coquand's calculus of constructions

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Coquand's calculus of constructions: A mathematical foundation for a proof development system

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1201296)