Type Theories from Barendregt’s Cube for Theorem Provers
From MaRDI portal
Publication:5251190
DOI10.1007/978-94-007-7548-0_7zbMath1344.03015OpenAlexW107734836MaRDI QIDQ5251190
Publication date: 22 May 2015
Published in: Trends in Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-94-007-7548-0_7
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Uses Software
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
- A Gentzen-style sequent calculus of constructions with expansion rules
- Extensional Set Equality in the Calculus of Constructions
- On lists and other abstract data types in the calculus of constructions
- A semantic model of types and machine instructions for proof-carrying code
- Inductively defined types in the Calculus of Constructions
- On the proof theory of Coquand's calculus of constructions
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Type Theories from Barendregt’s Cube for Theorem Provers