Postdoc: Proyecto ALAL

Como anuncié en un post anterior, se aproxima mi defensa de tesis: el 23 de Setiembre. A partir de Octubre comenzaré un postdoc en la Université de Paris-Nord (Paris XIII), un proyecto financiado por DIGITEO y la región Île-de-France. El responsable del proyecto de Michele Pagani, del Laboratoire d'Informatique de Paris Nord y el socio Gilles Dowek, director de uno de los 5 dominios de investigación del INRIA.

Título del proyecto: 

ALAL: Algebraic approaches to lambda calculi

(Métodos algebraicos para cálculos lambda)

No voy a poner el proyecto entero acá, pero dejo el resumen corto (abajo la traducción al español)

The project focuses on formal foundations for language-based (especially static) techniques guaranteeing resource-related runtime properties of programs. The project belongs to the research area whose aim is to associate to a program a certification assuring some specific properties. We will derive the tools and techniques for our investigation from the field of logical proof-theory and semantics, with special interest in linear logic and λ-calculus. In particular, we will explore the new interactions between linear algebra and the formal methods approach to computation, recently arisen from the differential extension of linear logic and the algebraic λ-calculi. The expected result is a robust theoretical framework in which to develop static analysis and verification tools for non-deterministic paradigms, such as stochastic systems, concurrent computation, quantum programming, etc.

Y aquí una traducción:

El proyecto se centra en los fundamentos formales de las técnicas basadas en lenguaje (sobre todo estáticas) que garantizan propiedades de ejecución de los programas relacionadas con recursos. Este proyecto pertenece al área de investigación cuyo objetivo es asociar a un programa una certificación que garantice ciertas propiedades. Vamos a derivar las herramientas y técnicas de nuestra investigación del campo de la teoría de la demostración lógica y de la semántica, con especial interés en lógica lineal y cálculo lambda. En particular, vamos a explorar las nuevas interacciones entre álgebra lineal y enfoques de métodos formales recientemente surgidos a partir de la extensión diferencial de lógica lineal y de los cálculos lambda algebraicos. El resultado esperado es un framework sólido en el cual desarrollar herramientas de análisis estático y verificación para paradigmas no-determinísticos como sistemas estocásticos, computación concurrente, computación cuántica, etc.

LSFA (y QuAND!)

Con Pablo Buiras, a quien estoy dirigiendo en su tesis de licenciatura (el equivalente a la tesis de master en el sistema de la Unión Europea) y Mauro Jaskelioff, su codirector, hemos escrito un paper basado en la tesis de Pablo, que fue aceptado en LSFA 2011. Será Pablo quien lo presente allí.

El paper aborda el problema de la confluencia del lambda cálculo algebraico lineal por medio de un sistema de tipos (el cual permite sólo términos fuertemente normalizables, lo que en conjunto con la confluencia local, nos da la confluencia del lenguaje). Este sistema de tipos puede verse como una extensión de Additive al cálculo completo o como una simplificación de Vectorial. Tiene la ventaja de que, al igual que Additive, sólo introduce sumas en los tipos, y no escalares como lo hace Vectorial, lo cual lo haría mucho más complejo y difícil de interpretar en otros sistemas conocidos. Además, da información aproximada de qué es lo que está pasando en el término: por ejemplo, si tenemos un término 2.1 M + 1.5 N donde M tiene tipo T y N tipo R, el tipo de esta combinación lineal de términos será T+T+R, dicho de otro modo, el tipo "aproxima las cantidades" de términos de cada tipo que están presentes en la combinación, tomando su parte entera.

El paper completo (el borrador, claro, aún tenemos tiempo para enviar la versión definitiva) lo pueden bajar de acá. Y el lunes pasado presenté el trabajo (con un cambio, ya que en mi presentación la normalización fuerte la derivo a partir de la normalización fuerte de Vectorial) en el encuentro del proyecto QuAND. Los slides de esa presentación están acá.

La versión definitiva del paper será publicada en el Electronic Proceedings in Theoretical Computer Science, una revista científica electrónica que suele publicar los anales de workshops y conferencias, y que tiene la particularidad de ser abierta: cualquiera puede descargarse sus artículos, no hace falta pagar por ello.

Update 25/03/12: Los proceedings del workshop han aparecido. Pueden bajar la versión publicada del paper desde aquí.

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.