Strong normalization of ^Sym_Prop- and ^-calculi

DOI10.23638/LMCS-13(3:34)2017MaRDI QIDQ5367073zbMATH OpenFDO

Authors Péter Battyányi, Karim Nour

Publication date 12 October 2017

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

zbMATH Keywords

\(\lambda^{\mathrm{Sym}}_{\mathrm{Prop}}\)-calculus\(\overline{\lambda}\mu\overline{\mu}^\ast\)-calculusarithmetical proofstrong normalization, classical logiczoom-in sequences of redexes

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Abstract: In this paper we give an arithmetical proof of the strong normalization of lambda-Sym-Prop of Berardi and Barbanera [1], which can be considered as a formulae-as-types translation of classical propositional logic in natural deduction style. Then we give a translation between the lambda-Sym-Prop-calculus and the lambda-bar-mu-mu-tilde-star-calculus, which is the implicational part of the lambda-bar-mu-mu-tilde-calculus invented by Curien and Herbelin [3] extended with negation. In this paper we adapt the method of David and Nour [4] for proving strong normalization. The novelty in our proof is the notion of zoom-in sequences of redexes, which leads us directly to the proof of the main theorem.

Recommendations

• Arithmetical proofs of strong normalization results for symmetric lambda calculi
• Typed Lambda Calculi and Applications
• 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
• Foundations of Software Science and Computation Structures

Cited in

(15)

• Strong normalization of a symmetric lambda calculus for second-order classical logic
• Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus
• Normalization proofs for the un-typed \(\mu\mu^\prime\)-calculus
• \(\lambda \rho\)-calculus. II
• scientific article; zbMATH DE number 1670497 (Why is no real title available?)
• scientific article; zbMATH DE number 2185704 (Why is no real title available?)
• Arithmetical proofs of strong normalization results for symmetric lambda calculi
• scientific article; zbMATH DE number 2080223 (Why is no real title available?)
• scientific article; zbMATH DE number 1377712 (Why is no real title available?)
• Asymptotically almost all \lambda-terms are strongly normalizing
• Foundations of Software Science and Computation Structures
• Typed Lambda Calculi and Applications
• Normalization in the simply typed -calculus
• Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage

This page was built for publication: Strong normalization of \(\lambda^{\mathrm{Sym}}_{\mathrm{Prop}}\)- and \(\overline{\lambda}\mu\overline{\mu}^\ast\)-calculi

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