Types 2010

Ya está publicada la lista de charlas y cronograma de Types 2010. Yo presentaré dos charlas allí:

• Sumas en cálculos lambda algebraicos. Un trabajo conjunto con Barbara Petit. En este trabajo definimos el fragmento (confluente) "aditivo" del Linear-Algebraic Lambda-Calculus. Le definimos un sistema de tipos que incluye sumas de tipos como reflejo de las sumas en los términos. Luego de probar subject reduction y strong normalisation, estudiamos el rol de las sumas en el cálculo interpretando nuestro sistema en System F con pares. Mostramos que este cálculo se puede interpretar como System F con un constructor de pares asociativo y conmutativo, el cual es distributivo con respecto a la aplicación.
• Un sistema de tipos vectorial. Un trabajo en colaboración con Pablo Arrighi y Benoît Valiron. El objetivo de este trabajo es combinar Scalar con Additive (el de más arriba) para crear un sistema de tipos al estilo System F para el Linear-Algebraic Lambda-Calculus el cual nos de una teoría de tipos general y original donde los tipos, de la misma manera que los términos, tengan una estructura de espacio vectorial. Mencionamos las conexiones con computación cuántica.

Luego de las charlas subiré aquí los slides. Aquí están.