On the proof theory of Coquand's calculus of constructions
From MaRDI portal
Publication:5961667
DOI10.1016/S0168-0072(96)00008-5zbMath0873.03048OpenAlexW2059912506MaRDI QIDQ5961667
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
arithmeticcalculus of constructionsnatural deduction systemstrong normalizationclassical logictyped lambda calculuspower sets
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