Confluency property of the call-by-value ^-calculus

MaRDI QIDQ3576003zbMATH OpenFDO

Authors Khelifa Saber, Karim Nour

Publication date 28 July 2010

Full work available at URL https://arxiv.org/abs/0905.1102, https://www.dmtcs.org/dmtcs-ojs/index.php/proceedings/article/view/dmAF0108/0.html

zbMATH Keywords

call-by-valueChurch-Rosser propertycomplete developmentparallel reductionpropositional classical logic

Mathematics Subject Classification ID

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

Abstract: In this paper, we introduce the $lambdam{u}^{wedgevee}$- call-by-value calculus and we give a proof of the Church-Rosser property of this system. This proof is an adaptation of that of Andou which uses an extended parallel reduction method and complete development.

Recommendations

• Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus
• Some properties of the \(\lambda\mu^{\wedge\vee}\)-calculus
• Parallel reduction in type free lambda/mu-calculus
• scientific article; zbMATH DE number 1499104
• Church–Rosser Made Easy

Cited in

(7)

• Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus
• Confluence proofs of lambda-mu-calculi by Z theorem
• Parallel reduction in type free lambda/mu-calculus
• scientific article; zbMATH DE number 1499104 (Why is no real title available?)
• Some properties of the \(\lambda\mu^{\wedge\vee}\)-calculus
• Procedural isomorphism, analytic information and  -conversion by value
• Z property for the shuffling calculus

This page was built for publication: Confluency property of the call-by-value \(\lambda\mu^{\wedge\vee}\)-calculus

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