Arithmetical proofs of strong normalization results for symmetric lambda calculi

zbMATH Open1122.03008arXiv0905.0762MaRDI QIDQ3593501FDOQ3593501

Authors: René David, Karim Nour 

Publication date: 20 July 2007

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.

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

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

zbMATH Keywords

strong normalizationclassical logicsymmetric lambda calculus

Mathematics Subject Classification ID

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

Cited In (15)

• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Typed Lambda Calculi and Applications
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
• Strong normalization of a symmetric lambda calculus for second-order classical logic
• Strong normalization theorems for quantized \(\lambda \)-calculi
• An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus
• 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)