Automath Type Inclusion in Barendregt’s Cube

DOI10.1007/978-3-319-20297-6_17zbMath1466.68078OpenAlexW1094406838MaRDI QIDQ3194722

Fairouz Kamareddine, J. B. Wells, Daniel Lima Ventura

Publication date: 20 October 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-20297-6_17

zbMATH Keywords

Automathunicity of typestype inclusion

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)

Uses Software

• Automath

Cites Work

• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations
• Zur Deutung der intuitionistischen Logik
• The Barendregt cube with definitions and generalised reduction
• Canonical typing and ∏-conversion in the Barendregt Cube
• Pure subtype systems
• Typed $\lambda$-calculi with one binder
• Subtyping dependent types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item