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

Alejandro Díaz-Caro 1, * Barbara Petit 2
* Auteur correspondant
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.
Type de document :
Communication dans un congrès
Luke Ong and Ruy de Queiroz. WoLLIC - 19th International Workshop on Logic, Language, Information and Computation - 2012, Sep 2012, Buenos Aires, Argentina. Springer, 7456, pp.216-231, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-32621-9_16〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00924992
Contributeur : Alejandro Díaz-Caro <>
Soumis le : mardi 7 janvier 2014 - 13:50:44
Dernière modification le : samedi 27 janvier 2018 - 01:31:47

Lien texte intégral

Identifiants

Citation

Alejandro Díaz-Caro, Barbara Petit. Linearity in the non-deterministic call-by-value setting. Luke Ong and Ruy de Queiroz. WoLLIC - 19th International Workshop on Logic, Language, Information and Computation - 2012, Sep 2012, Buenos Aires, Argentina. Springer, 7456, pp.216-231, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-32621-9_16〉. 〈hal-00924992〉

Partager

Métriques

Consultations de la notice

244