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

DOI10.1007/3-540-60579-7_2MaRDI QIDQ6083893zbMATH OpenOpenAlexFDO

Authors 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

conversion ruleinductive typesoundness theoremstrong normalizationtype constructor

Mathematics Subject Classification ID

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

Cites work

• (In)consistency of Extensions of Higher Order Logic and Type Theory
• scientific article; zbMATH DE number 4191621 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3695144 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3513750 (Why is no real title available?)
• scientific article; zbMATH DE number 1555189 (Why is no real title available?)
• scientific article; zbMATH DE number 1400716 (Why is no real title available?)
• scientific article; zbMATH DE number 3247154 (Why is no real title available?)
• Modularity of strong normalization in the algebraic-λ-cube
• Strong normalization in type systems: A model theoretical approach
• The calculus of constructions
• The lambda calculus, its syntax and semantics

Cited in

(1)

• Congruence types

This page was built for publication: A short and flexible proof of strong normalization for the calculus of constructions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6083893)