Strong normalization results by translation

DOI10.1016/J.APAL.2010.02.002MaRDI QIDQ636353zbMATH OpenOpenAlexFDO

Authors René David, Karim Nour

Publication date 26 August 2011

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2010.02.002

zbMATH Keywords

\(\lambda \mu \)-calculusclassical logicrecursive equationsstrong normalization

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Strong normalization of classical natural deduction with disjunctions
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• A short proof of the strong normalization of classical natural deduction with disjunction
• A note on strong normalization in classical natural deduction
• Strong normalization proofs by CPS-translations

Cites work

• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• A short proof of the strong normalization of classical natural deduction with disjunction
• An Arithmetical Proof of the Strong Normalization for the λ-Calculus with Recursive Equations on Types
• scientific article; zbMATH DE number 1722654 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• Inductive types and type constraints in the second-order lambda calculus
• Non-strictly positive fixed points for classical natural deduction
• Proofs of strong normalisation for second order classical natural deduction
• Short Proofs of Strong Normalization
• Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
• Stabilization -- an alternative to double-negation translation for classical natural deduction
• Strong normalization of classical natural deduction with disjunctions

Cited in

(7)

• Strong normalization of classical natural deduction with disjunctions
• scientific article; zbMATH DE number 1722654 (Why is no real title available?)
• Proving strong normalisation via non-deterministic translations into Klop's extended lambda-calculus
• scientific article; zbMATH DE number 2185704 (Why is no real title available?)
• A note on strong normalization in classical natural deduction
• Strong normalization for truth table natural deduction
• Strong normalization proofs by CPS-translations

This page was built for publication: Strong normalization results by translation

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