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

DOI10.1007/978-3-642-32621-9_16MaRDI QIDQ2915029zbMATH OpenOpenAlexFDO

Authors Alejandro Díaz-Caro, Barbara Petit

Publication date 21 September 2012

Published in Logic, Language, Information and Computation (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

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.

Recommendations

• Call-by-value non-determinism in a linear logic type discipline
• A non-deterministic call-by-need lambda calculus
• A Linear-non-Linear Model for a Computational Call-by-Value Lambda Calculus (Extended Abstract)
• scientific article; zbMATH DE number 1231468
• A non-deterministic call-by-need lambda calculus

Cited in

(14)

• A concrete categorical semantics of lambda-\(\mathcal{S}\)
• A relational account of call-by-value sequentiality
• Call-By-Push-Value from a Linear Logic Point of View
• Call-by-value non-determinism in a linear logic type discipline
• Typing Quantum Superpositions and Measurement
• A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls
• Proof normalisation in a logic identifying isomorphic propositions
• The vectorial \(\lambda\)-calculus
• Non-linearity as the metric completion of linearity
• Extensional proofs in a propositional logic modulo isomorphisms
• A concrete model for a typed linear algebraic lambda calculus
• A quick overview on the quantum control approach to the lambda calculus
• A linear linear lambda-calculus
• A linear proof language for second-order intuitionistic linear logic

This page was built for publication: Linearity in the non-deterministic call-by-value setting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2915029)