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

MaRDI QIDQ2851698zbMATH OpenFDO

Authors René David, Karim Nour

Publication date 2 October 2013

Full work available at URL https://arxiv.org/abs/0905.1554, http://www.sciencedirect.com/science/article/pii/S1571066105051303

Mathematics Subject Classification ID

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

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.

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

Cited in

(5)

• Classical \(F_{\omega}\), orthogonality and symmetric candidates
• 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

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)