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

MaRDI QIDQ3576003zbMATHFDO

Authors Khelifa Saber, Karim Nour

Publication date 28 July 2010

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

zbMATH Keywords

call-by-valueChurch-Rosser propertyparallel reductionpropositional classical logiccomplete development

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

(5)

• Z property for the shuffling calculus
• Some properties of the \(\lambda\mu^{\wedge\vee}\)-calculus
• Parallel reduction in type free lambda/mu-calculus
• Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus
• Procedural isomorphism, analytic information and  -conversion by value

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)