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

zbMATH Open1193.03032arXiv0905.1102MaRDI QIDQ3576003FDOQ3576003

Authors: Khelifa Saber, Karim Nour 

Publication date: 28 July 2010

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.

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

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

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)

Cited In (5)

• Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus
• Z property for the shuffling calculus
• Some properties of the \(\lambda\mu^{\wedge\vee}\)-calculus
• Parallel reduction in type free 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)