Linearity in the non-deterministic call-by-value setting

Abstract

We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F with pairs, which corresponds to a non linear fragment of linear logic. The translation provides a deeper understanding of the linearity in our setting.

15 pages. To appear in WoLLIC 2012

References in corpus (1)

• Non determinism through type isomorphism

Cited by in corpus (11)

• The Vectorial $\lambda$-Calculus
• Two linearities for quantum computing in the lambda calculus
• Realizability in the Unitary Sphere
• A linear linear lambda-calculus
• A Type System for the Vectorial Aspect of the Linear-Algebraic Lambda-Calculus
• Non determinism through type isomorphism
• A lambda calculus for density matrices with classical and probabilistic controls
• The probability of non-confluent systems
• A linear proof language for second-order intuitionistic linear logic
• Extensional proofs in a propositional logic modulo isomorphisms
• A Quick Overview on the Quantum Control Approach to the Lambda Calculus