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

DOI10.1007/BF01211392zbMATH Open0766.03007OpenAlexW2012195956MaRDI QIDQ1201296FDOQ1201296

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

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

zbMATH Keywords

normalisationcalculus of constructionsconsistency of assumptionshigher order typed \(\lambda\)-calculusproof development system

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Combinatory logic. With two sections by William Craig.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The calculus of constructions
• Combinatory logic. Vol. II
• On the proof theory of Coquand's calculus of constructions
• Title not available (Why is that?)
• A transfinite type theory with type variables
• A sequent calculus for type assignment

Cited In (15)

• Title not available (Why is that?)
• Verified representations of Landau's ``Grundlagen in the \(\lambda\delta\) family and in the calculus of constructions
• A Gentzen-style sequent calculus of constructions with expansion rules
• A mechanized proof system of the third generation calculus in Coq
• Interpreting HOL in the calculus of constructions
• Variants of the basic calculus of constructions
• Type theories from Barendregt's cube for theorem provers
• Title not available (Why is that?)
• The calculus of constructions
• A modular construction of type theories
• Title not available (Why is that?)
• The calculus of constructions as a framework for proof search with set variable instantiation
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the proof theory of Coquand's calculus of constructions

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)