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
Liste complète des métadonnées

https://hal.inria.fr/hal-00924992
Contributor : Alejandro Díaz-Caro <>
Submitted on : Tuesday, January 7, 2014 - 1:50:44 PM
Last modification on : Wednesday, February 6, 2019 - 1:26:07 AM

Links full text

Identifiers

Citation

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⟩

Share

Metrics

Record views

252