Talk @ Paris 13

(English version below)

El próximo 17 de enero daré una charla sobre los sistemas de tipos algebraicos en Paris 13 (Lab LIPN) en las series "Sémiraires LCR". Aquí está la información y aquí reproduzco el resumen:

En esta charla voy a presentar varias extensiones a System F, para tipar el lambda-cálculo lineal-algebraico, un lambda-cálculo enriquecido con una estructura vectorial. El primer sistema de tipos es una extensión directa de System F, el cual sólo tipa el cálculo sin más adorno. El segundo es un sistema de tipos que tiene en cuenta escalares, el cual puede servir como una garantía de que la forma normal de un término tiene forma con . El siguiente sistema incluye "suma de tipos" reflejando los de los términos -- mostrando que las sumas en el cálculo algebraico se comportan como una clase particular de pares. Finalmente el último sistema de tipos combina los dos anteriores. Damos contraejemplos de porqué este tipo de sistema de tipos vectorial no se puede hacer en estilo Curry y mostramos algunas pistas de un futuro sistema de tipos vectorial en estilo Church, adecuado para especializarlo en un cálculo cuántico.

Edit: Aquí dejo los slides.

---

Next January 17th I will give a talk about the algebraic type systems at Paris 13 (LIPN Lab) in the series "Sémiraires LCR". Here it is the information and I reproduce here the abstract:

In this talk I will present several extensions to the System F, for the sake of type the linear-algebraic lambda-calculus, a lambda-calculus enriched with a vectorial structure. The first type system is a straightforward extension of System F, which just types the calculus without any further adornment. The second one is a type system accounting for scalars, which can serve as a guarantee that the normal form of a term is of the form with . The following system includes "sums of types" reflecting that of the terms--showing that sums in the algebraic calculus behaves as a special kind of pairs. Eventually the last type system combines the previous two. We give counterexamples of why this kind of vectorial type system cannot be made in Curry style and show the clues of a future vectorial type system in Church style suitable to specialize the calculus into a quantum calculus.

Edit: Here are the slides.