Non Deterministic Classical Logic: Theλμ++ -calculus
Karim Nour · Mathematical logic quarterly · 2002
In this paper, we present an extension of λμ-calculus called λμ++-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.