3 de enero de 2013

LFCS @ San Diego

Este sábado salgo para San Diego, California, EE.UU. para participar del Simposio sobre Fundamentos Lógicos de las Ciencias de la Computación (Symposium on Logical Foundations of Computer Science, LFCS). Allí fue aceptado el paper que escribimos con Giulio Manzonetto y Michele Pagani y que comenté rápidamente en este post. A la vuelta les comento sobre el simposio y dejo mis slides de la presentación. El paper saldrá salió publicado en el volume 7734 de LNCS, y, como siempre, pueden también bajarlo libremente desde mi página web. Les dejo el título y abstract en inglés:
Call-by-value non-determinism in a linear logic type discipline
We consider the call-by-value λ-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 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. 
Update: Aquí les dejo los slides que usé en la presentación, y el link al paper en la página de Springer (y les repito el link al PDF que se puede descargar desde mi página web sin necesidad de pagarle a Springer).
El simposio estuvo interesante en general, aunque quizá demasiado orientado hacia justification logic para mi gusto.