Computación cuántica, lambda-cálculo, lógica... y todo eso

Este año estoy trabajando en un centro INRIA y dando clases en la Universidad Paris-Ouest, integrando un grupo de matemáticos. Yo soy informático teórico, no matemático, y es por eso que la investigación la hago en el INRIA.

La semana pasada, dí una charla para el grupo de la universidad. La idea era dar un panorama general de qué es lo que investigo. Dado que el público no conocía computación cuántica, lambda-cálculo, ni nada de los temas que yo trabajo en general, la charla se trató de hacer una introducción a todos esos temas y luego contar un poco, de forma bastante genérica, dónde entrarían mis temas de investigación actuales.

Este post es simplemente para dejarles los slides por si a alguno le interesa. Claro que arriba de los post también hablé, por lo que faltarán detalles. Pero si alguno de los lectores de este blog está interesado en saber un poco de qué se trata todo eso de cuántica, lambda-cálculo y lógica, pues aquí va.

Aquí les dejo también el link directo al PDF

Emalca Salta 2013

Saliendo un poco del letargo de los últimos meses donde he estado inmerso en escribir mi tesis, esta entrada la escribo para promocionar la escuela EMALCA 2013 en Salta, Argentina.

Escuela de Matemática de América Latina y el Caribe

Yo he participado en la edición 2005 que se llevó a cabo en Paraguay. Los cursos son de diferentes niveles y para todos los gustos. En esta edición me llama la atención el curso sobre Cadenas de Markov, uno de mis eternos temas favoritos.

Espero que a algún lector le parezca interesante y decida ir.

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.