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.

DCM 2011

Luego de un período de larga ausencia del blog (me excuso con que estaba terminando de redactar mi tesis (la cual se encuentra en revisión por el jurado ahora)) vuelvo para comentarles que este domingo estaré presentando un paper en el 7th International Workshop on Developments of Computational Models (el 3 de Julio, en Zúrich). El paper es un trabajo en conjunto con Pablo Arrighi y Benoît Valiron, el cual presenté antes en algunos encuentros informales y ahora fue aceptado para ser publicado en los proceedings de este workshop.

Les dejo los detalles originales en inglés y debajo la traducción.

A type system for the vectorial aspects of the linear-algebraic lambda-calculus

(joint work with Pablo Arrighi and Benoît Valiron)

We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors, i.e. it is able to statically describe the linear combinations of terms resulting from the reduction of programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We show that the resulting typed lambda-calculus is strongly normalizing and features a weak subject-reduction.

Un sistema de tipos para los aspectos vectoriales del lambda cálculo algebraico lineal

(trabajo en conjunto con Pablo Arrighi y Benoît Valiron)

Describimos un sistema de tipos para el lambda cálculo algebraico lineal. El sistema de tipos tiene en cuenta la parte del lenguaje que emula operadores lineales y vectores, o sea, es capaz de describir estáticamente las combinaciones lineales de términos resultantes de la reducción de los programas. Esto conduce a una teoría de tipos original donde los tipos, de la misma manera que los términos, pueden ser superpuestos en combinaciones lineales. Mostramos que el cálculo tipado resultante tiene normalización fuerte y una versión débil de la propiedad de conservación de tipo.

Hasta que esté publicado (en EPTCS, de libre acceso), les dejo aquí los links: (ver más abajo)

• Versión oficial de 12 páginas (preprint)
• Versión completa con todas las pruebas en apéndice

Luego del workshop subiré aquí los slides de la presentación también.

Update (05/07/11): Aquí están los slides que presenté durante el workshop.

Update (31/07/12): Finalmente el paper está online (y es de libre acceso): EPTCS.

Poster para la escuela

Este domingo me pongo en camino al 11th Summer School on Quantum Information & 8th Canadian Student Conference on Quantum Information, como lo mencioné en el post anterior.

Por lo tanto, aquí está el poster que voy a presentar allí (enlace). No es perfecto, siempre mi punto débil fue el diseño de posters y presentaciones. Pero, es lo suficientemente bueno para transmitir la idea, lo cual es lo más importante.

No creo que vaya a escribir durante mi estadía allá, pero si seguramente estaré dando algunos avisos por el twitter. Al regresar voy a escribir sobre mis impresiones. Después de más de 3 años por Asia, voy a volver a un uso horario Americano.

Ahh, si a alguien le interesa el tema de investigación del poster, dejen un comentario, y puedo explicar sobre que es. Básicamente, son dos cotas superiores en una generalización de la distancia de Hamming. Como aún es un trabajo en progreso, sigo buscando las cotas inferiores para el problema. A ver si puedo conseguir un poco de feedback en la escuela.