Skip to Main content Skip to Navigation
New interface
Conference papers

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

Alejandro Díaz-Caro 1, * Barbara Petit 2 
* Corresponding author
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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.
Document type :
Conference papers
Complete list of metadata
Contributor : Alejandro Díaz-Caro Connect in order to contact the contributor
Submitted on : Tuesday, January 7, 2014 - 1:50:44 PM
Last modification on : Thursday, February 3, 2022 - 3:43:27 AM

Links full text



Alejandro Díaz-Caro, Barbara Petit. Linearity in the non-deterministic call-by-value setting. WoLLIC - 19th International Workshop on Logic, Language, Information and Computation - 2012, Sep 2012, Buenos Aires, Argentina. pp.216-231, ⟨10.1007/978-3-642-32621-9_16⟩. ⟨hal-00924992⟩



Record views