Why the usual candidates of reducibility do not work for the symmetric -calculus

zbMATH Open1272.68082arXiv0905.1554MaRDI QIDQ2851698FDOQ2851698

Authors: René David, Karim Nour 

Publication date: 2 October 2013

Abstract: The symmetric $lambdamu$-calculus is the $lambdamu$-calculus introduced by Parigot in which the reduction rule $m{u}^{\prime }$, which is the symmetric of $mu$, is added. We give examples explaining why the technique using the usual candidates of reducibility does not work. We also prove a standardization theorem for this calculus.

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

Recommendations

• Typed Lambda Calculi and Applications
• Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus
• scientific article; zbMATH DE number 2242601
• Foundations of Software Science and Computation Structures
• On the Relations between the Syntactic Theories of λμ-Calculi

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Cited In (5)

• Abstracting models of strong normalization for classical calculi
• An estimation for the lengths of reduction sequences of the \(\lambda\mu\rho\theta\)-calculus
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
• An encoding of the \(\lambda \)-calculus in the string MultiSet rewriting calculus
• Classical \(F_{\omega}\), orthogonality and symmetric candidates

This page was built for publication: Why the usual candidates of reducibility do not work for the symmetric \(\lambda\mu\)-calculus

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