Two different strong normalization proofs?

DOI10.1007/3-540-61254-8_27zbMath1434.03130OpenAlexW2111361742MaRDI QIDQ4645812

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

finite typeformal proofexistential quantifierreduction sequencepredicate symbol

Mathematics Subject Classification ID

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

Cites Work

• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Intensional interpretations of functionals of finite type I
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Two different strong normalization proofs?