Confluency property of the call-by-value $\lambda\mu^{\wedge \vee}$-calculus

TL;DR

This paper introduces a call-by-value calculus for the lambda-mu system with conjunction and disjunction, proving its Church-Rosser property using an adapted parallel reduction method.

Contribution

It presents the first call-by-value $ ext{lambda} ext{-} ext{mu}^{ ext{wedge} ext{vee}}$-calculus and proves its confluence, extending previous methods to this new system.

Findings

The calculus satisfies the Church-Rosser property.

The proof adapts extended parallel reduction techniques.

Establishes foundational properties for this calculus.

Abstract

In this paper, we introduce the $\lambda\mu^{\wedge \vee}$- 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.