Call-by-value non-determinism in a linear logic type discipline
Logic in Computer Science
2014-01-08 v1
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.
Keywords
Cite
@article{arxiv.1312.4507,
title = {Call-by-value non-determinism in a linear logic type discipline},
author = {Alejandro Díaz-Caro and Giulio Manzonetto and Michele Pagani},
journal= {arXiv preprint arXiv:1312.4507},
year = {2014}
}