A short and flexible proof of strong normalization for the calculus of constructions

DOI10.1007/3-540-60579-7_2zbMath1530.03058OpenAlexW2103033459MaRDI QIDQ6083893

Herman Geuvers

Publication date: 8 December 2023

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

Full work available at URL: https://research.tue.nl/nl/publications/3619121e-2a08-4571-80a7-0eabbc7a4f7d

zbMATH Keywords

strong normalizationtype constructorsoundness theoreminductive typeconversion rule

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Cites Work

• The calculus of constructions
• The lambda calculus, its syntax and semantics
• Strong normalization in type systems: A model theoretical approach
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• Modularity of strong normalization in the algebraic-λ-cube
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item