Non deterministic classical logic: the $\lambda\mu^{++}$-calculus

TL;DR

This paper introduces the $\lambda\mu^{++}$-calculus, an extension of $\lambda\mu$-calculus, featuring properties like strong normalization, data representation uniqueness, and the ability to program parallel-or, enhancing classical logic modeling.

Contribution

It presents a novel extension of $\lambda\mu$-calculus with key properties and parallel-or programming capabilities, advancing classical logic computational frameworks.

Findings

Ensures subject reduction and strong normalization.

Guarantees unicity of data representation and confluence on data types.

Enables programming of parallel-or within the calculus.

Abstract

In this paper, we present an extension of $\lambda\mu$-calculus called $\lambda\mu^{++}$-calculus which has the following properties: subject reduction, strong normalization, unicity of the representation of data and thus confluence only on data types. This calculus allows also to program the parallel-or.