Two \textit{different} strong normalization proofs?

DOI10.1007/3-540-61254-8_27MaRDI QIDQ4645812zbMATH OpenOpenAlexFDO

Authors Jaco van de Pol

Publication date 11 January 2019

Published in Higher-Order Algebra, Logic, and Term Rewriting (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61254-8_27

zbMATH Keywords

existential quantifierfinite typeformal proofpredicate symbolreduction sequence

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Higher-type and set recursion theory (03D65) Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 4045709
• scientific article; zbMATH DE number 512774
• Program extraction from proofs of weak head normalization
• Short Proofs of Strong Normalization
• Program extraction from normalization proofs

Cites work

• scientific article; zbMATH DE number 2185672 (Why is no real title available?)
• scientific article; zbMATH DE number 4045709 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard

Cited in

(4)

• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• scientific article; zbMATH DE number 3950521 (Why is no real title available?)
• scientific article; zbMATH DE number 4055611 (Why is no real title available?)
• scientific article; zbMATH DE number 1088210 (Why is no real title available?)

This page was built for publication: Two \textit{different} strong normalization proofs?

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