On the proof theory of Coquand's calculus of constructions

DOI10.1016/S0168-0072(96)00008-5zbMath0873.03048OpenAlexW2059912506MaRDI QIDQ5961667

Jonathan P. Seldin

Publication date: 26 February 1997

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(96)00008-5

zbMATH Keywords

arithmeticcalculus of constructionsnatural deduction systemstrong normalizationclassical logictyped lambda calculuspower sets

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03) Combinatory logic and lambda calculus (03B40)

Related Items (9)

An epistemic logic for becoming informed ⋮ Interpreting HOL in the calculus of constructions ⋮ Variants of the basic calculus of constructions ⋮ Pure type systems with more liberal rules ⋮ Flag-based big-step semantics ⋮ Coquand's calculus of constructions: A mathematical foundation for a proof development system ⋮ A Gentzen-style sequent calculus of constructions with expansion rules ⋮ Equivalences between pure type systems and systems of illative combinatory logic ⋮ Type Theories from Barendregt’s Cube for Theorem Provers

Cites Work

• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• The calculus of constructions
• Coquand's calculus of constructions: A mathematical foundation for a proof development system
• Combinatory logic. Vol. II
• Combinators, \(\lambda\)-terms and proof theory
• A sequent calculus for type assignment
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the proof theory of Coquand's calculus of constructions