Call-by-value non-determinism in a linear logic type discipline

Abstract : We consider the call-by-value lambda-calculus extended with a may-convergent non-deterministic choice and a must-convergent parallel composition. Inspired by recent works on the relational semantics of linear logic and non-idempotent intersection types, we endow this calculus with a type system based on the so-called Girard's second translation of intuitionistic logic into linear logic. We prove that a term is typable if and only if it is converging, and that its typing tree carries enough information to give a bound on the length of its lazy call-by-value reduction. Moreover, when the typing tree is minimal, such a bound becomes the exact length of the reduction.
Type de document :
Communication dans un congrès
Sergei Artemov and Anil Nerode. LFCS - Logical Foundations of Computer Science - 2013, Jan 2013, San Diego, CA, United States. Springer, 7734, pp.164-178, 2013, Lecture Notes in Computer Science. <10.1007/978-3-642-35722-0_12>
Liste complète des métadonnées


https://hal.inria.fr/hal-00919463
Contributeur : Alejandro Díaz-Caro <>
Soumis le : lundi 16 décembre 2013 - 17:58:06
Dernière modification le : mardi 11 octobre 2016 - 14:54:34
Document(s) archivé(s) le : samedi 8 avril 2017 - 07:12:19

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Alejandro Díaz-Caro, Giulio Manzonetto, Michele Pagani. Call-by-value non-determinism in a linear logic type discipline. Sergei Artemov and Anil Nerode. LFCS - Logical Foundations of Computer Science - 2013, Jan 2013, San Diego, CA, United States. Springer, 7734, pp.164-178, 2013, Lecture Notes in Computer Science. <10.1007/978-3-642-35722-0_12>. <hal-00919463>

Partager

Métriques

Consultations de
la notice

323

Téléchargements du document

83