scientific article; zbMATH DE number 1301734

MaRDI QIDQ4246947zbMATH OpenFDO

Authors Jean Goubault-Larrecq

Publication date 13 December 1999

zbMATH Keywords

weak terminationsecond-order type systemreduction of simply-typed \(\lambda\sigma\)-termssimply-typed \(\lambda\)-calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 1342288
• The Weak Normalization of the Simply Typed  se-calculus
• Strong normalization of substitutions
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Rewriting Techniques and Applications

Cited in

(10)

• Proving weak properties of rewriting
• A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types
• Two decreasing measures for simply typed \(\lambda\)-terms
• The Weak Normalization of the Simply Typed  se-calculus
• Mechanical procedure for proof construction via closed terms in typed calculus
• scientific article; zbMATH DE number 6828930 (Why is no real title available?)
• Resource operators for \(\lambda\)-calculus
• Strong normalisation in \(\lambda \)-calculi with references
• The Safe Lambda Calculus
• Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves

This page was built for publication:

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