A simple model construction for the Calculus of Constructions

DOI10.1007/3-540-61780-9_74zbMath1434.03046OpenAlexW1528995598MaRDI QIDQ4647584

No author found.

Publication date: 15 January 2019

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

Full work available at URL: http://hdl.handle.net/2066/28269

zbMATH Keywords

strong normalizationclassical logicsoundness theoremdependent producttypable term

Mathematics Subject Classification ID

Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40) Type theory (03B38)

Related Items (1)

An intuitionistic set-theoretical model of fully dependent CC

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Independence of the induction principle and the axiom of choice in the pure calculus of constructions
• A higher-order calculus and theory abstraction
• Constructive natural deduction and its ‘ω-set’ interpretation
• An application of PER models to program extraction
• Collapsing partial combinatory algebras
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus

This page was built for publication: A simple model construction for the Calculus of Constructions