Strong normalization results by translation

DOI10.1016/J.APAL.2010.02.002zbMath1223.03037OpenAlexW2086157169MaRDI QIDQ636353

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

strong normalizationclassical logicrecursive equations\(\lambda \mu \)-calculus

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• Non-strictly positive fixed points for classical natural deduction
• Strong normalization of classical natural deduction with disjunctions
• Inductive types and type constraints in the second-order lambda calculus
• Short Proofs of Strong Normalization
• An Arithmetical Proof of the Strong Normalization for the λ-Calculus with Recursive Equations on Types
• Simple Saturated Sets for Disjunction and Second-Order Existential Quantification
• Proofs of strong normalisation for second order classical natural deduction
• A short proof of the strong normalization of classical natural deduction with disjunction

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