Arithmetical proofs of strong normalization results for symmetric lambda calculi

MaRDI QIDQ3593501zbMATH OpenFDO

Authors René David, Karim Nour

Publication date 20 July 2007

Full work available at URL https://arxiv.org/abs/0905.0762

zbMATH Keywords

strong normalizationclassical logicsymmetric lambda calculus

Mathematics Subject Classification ID

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

Abstract: We give arithmetical proofs of the strong normalization of two symmetric $lambda$-calculi corresponding to classical logic. The first one is the $$-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "call-by-value". The second one is the symmetric $lambdamu$-calculus. It is the $lambdamu$-calculus introduced by Parigot in which the reduction rule $m{u}^{\prime }$, which is the symmetric of $mu$, is added. These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical.

Recommendations

• Typed Lambda Calculi and Applications
• Strong normalization of \(\lambda^{\mathrm{Sym}}_{\mathrm{Prop}}\)- and \(\overline{\lambda}\mu\overline{\mu}^\ast\)-calculi
• Strong normalization of a symmetric lambda calculus for second-order classical logic
• A short proof of the strong normalization of classical natural deduction with disjunction
• scientific article; zbMATH DE number 2080223

Cited in

(17)

• scientific article; zbMATH DE number 1722654 (Why is no real title available?)
• Normalization proofs for the un-typed \(\mu\mu^\prime\)-calculus
• An Arithmetical Proof of the Strong Normalization for the λ-Calculus with Recursive Equations on Types
• An estimation for the lengths of reduction sequences of the \(\lambda\mu\rho\theta\)-calculus
• scientific article; zbMATH DE number 2080223 (Why is no real title available?)
• scientific article; zbMATH DE number 598799 (Why is no real title available?)
• Foundations of Software Science and Computation Structures
• Strong Normalization of the Dual Classical Sequent Calculus
• Normalization in the simply typed -calculus
• Computational and Information Science
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
• Typed Lambda Calculi and Applications
• Strong normalization of a symmetric lambda calculus for second-order classical logic
• Strong normalization theorems for quantized \(\lambda \)-calculi
• Strong normalization of \(\lambda^{\mathrm{Sym}}_{\mathrm{Prop}}\)- and \(\overline{\lambda}\mu\overline{\mu}^\ast\)-calculi
• \(\lambda \rho\)-calculus. II
• A normal form for arithmetical derivations implying the \(\omega\)-consistency of arithmetic

This page was built for publication: Arithmetical proofs of strong normalization results for symmetric lambda calculi

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