Habemus date definito : XXIII Septembris

(English below)

Mi tesis titulada "Du typage vectoriel" (Del tipage vectorial) ha sido aceptada para ser defendida. Hemos fijado la fecha de la defensa para el 23 de septiembre. Aquí la traducción del resumen oficial.

El objetivo de esta tesis es desarrollar una teoría de tipos para el λ-cálculo algebraico-lineal, una extensión de λ-cálculo motivada por la computación cuántica. Esta extensión algebraica comprende todos los términos del λ-cálculo y sus combinaciones lineales, de manera que si t y r son dos términos, α.t + β.r, con α y β escalares de un anillo dado, también lo es. La idea principal y el desafío de esta tesis ha sido introducir un sistema de tipos donde los tipos, de la misma manera que los términos, formen un espacio vectorial, proveyendo información acerca de la estructura de la forma normal de los términos. Esta tesis presenta el sistema Lineal, y también tres sistemas intermedios, aunque interesantes por ellos mismos: Scalar, Additive y λCA, todos ellos con sus pruebas de preservación de tipo y normalización fuerte.

Aquí les dejo el anuncio oficial. El manuscrito no lo voy a hacer público hasta que no corrija la enorme cantidad de errores de tipeo que tiene.

---

My thesis entitled "Du typage vectoriel" (On vectorial typing) has been accepted to be defended. The Viva has been fixed for the 23th September. Here you are the official abstract:

The objective of this thesis is to develop a type theory for the linear-algebraic λ-calculus, an extension of λ-calculus motivated by quantum computing. This algebraic extension encompass all the terms of λ-calculus together with their linear combinations, so if t and r are two terms, so is α.t + β.r, with α and β being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type system where the types, in the same way as the terms, form a vectorial space, providing the information about the structure of the normal form of the terms. This thesis presents the system Lineal, and also three intermediate systems, however interesting by themselves: Scalar, Additive and λCA, all of them with their subject reduction and strong normalisation proofs.

Here it is the official announcement. I won't make the manuscript public until I do not correct the huge amount of typos it has.