A schematic proof of strong normalization for the system of the -cube

MaRDI QIDQ3365535zbMATH OpenFDO

Authors Milena Stefanova

Publication date 23 January 2006

zbMATH Keywords

normalizationtyped lambda calculusinductive types

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Short Proofs of Strong Normalization
• Strong normalization in type systems: A model theoretical approach
• scientific article; zbMATH DE number 1301737
• scientific article; zbMATH DE number 512779
• Strong normalization from weak normalization in typed \(\lambda\)-calculi

Cited in

(4)

• Strong normalization in type systems: A model theoretical approach
• scientific article; zbMATH DE number 1692907 (Why is no real title available?)
• Weak normalization implies strong normalization in a class of non-dependent pure type systems
• A Formal Proof of the Strong Normalization Theorem for System T in Agda

This page was built for publication: A schematic proof of strong normalization for the system of the \(\lambda\)-cube

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