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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-00919463
Contributor : Alejandro Díaz-Caro <>
Submitted on : Monday, December 16, 2013 - 5:58:06 PM
Last modification on : Thursday, February 7, 2019 - 5:47:56 PM
Document(s) archivé(s) le : Saturday, April 8, 2017 - 7:12:19 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Alejandro Díaz-Caro, Giulio Manzonetto, Michele Pagani. Call-by-value non-determinism in a linear logic type discipline. LFCS - Logical Foundations of Computer Science - 2013, Jan 2013, San Diego, CA, United States. pp.164-178, ⟨10.1007/978-3-642-35722-0_12⟩. ⟨hal-00919463⟩

Share

Metrics

Record views

418

Files downloads

145