13 de septiembre de 2011

Soutenance / Defence / Defensa + QuAND

(English) (Español)


J'ai le plaisir de annoncer ma soutenance de thèse, accompagné d'un rencontre QuAND, qui aura lieu le 23 septembre à Grenoble. Voici le programme, les infos pratiques et les détails de la thèse.

PROGRAMME :

10h - 11h :
  Réunion stratégique du projet QuAND (privé)
11h15 - 12h :
  Exposé de Michele Pagani « Working for a theory of algebraic abstract reduction systems »
12h - 14h :
  Pause repas
14h30 - 16h :
  Soutenance de thèse d'Alejandro Díaz-Caro : « Du typage vectoriel »
16h :
  Pot de thèse

INFOS PRATIQUES :

Voilà un petit carte http://g.co/maps/rc8dc et quelques renseignements :
Depuis la gare vous pouvez prendre le Tram B direction « Plaine des sports » et descendre à l'arrêt « Bibliothèques universitaires ».
Le rencontre QuAND aura lieu à la Salle Aquarium, et la soutenance dans l'Amphi du MJK ( Maison Jean Kuntzmann ) même que le pot de thèse.


DÉTAILS DE LA THÈSE :

Titre :
Du typage vectoriel
Par :
Alejandro DÍAZ-CARO
Directeur :
Pablo ARRIGHI
Co-directeur :
Frédéric PROST

Cette soutenance aura lieu Vendredi 23 Septembre 2011 à 14h30 devant le jury composé de :

Rapporteurs :
Gilles DOWEK
Directeur de recherche - INRIA Centre Paris-Rocquencourt 
Thomas EHRHARD
Directeur de recherche CNRS - Laboratoire Preuves, Programmes et Systèmes 
Eduardo BONELLI
Profesor Asociado et Investigador Adjunto - Universidad Nacional de Quilmes et CONICET

Examinateurs :
Philippe JORRAND
Directeur de Recherche Émérite - CNRS
Laurent REGNIER
Professeur - Université de la Méditerranée
Lionel VAUX
Maitre de Conférences - Université de la Méditerranée
Michele PAGANI
Maitre de Conférences - Université de Paris Nord

Directeur de thèse :
Pablo ARRIGHI
Maitre de Conférences - Université de Grenoble

Résumé de la thèse
L'objectif de cette thèse est de développer une théorie de types pour le λ-calcul linéaire-algébrique, une extension du λ-calcul motivé par l'informatique quantique. Cette extension algébrique comprend tous les termes du λ-calcul plus leurs combinaisons linéaires, donc si t et r sont des termes, α.t+β.r est aussi un terme, avec α et β des scalaires pris dans un anneau. L'idée principale et le défi de cette thèse était d'introduire un système de types où les types, de la même façon que les termes, constituent un espace vectoriel, permettant la mise en évidence de la structure de la forme normale d'un terme. Cette thèse présente le système Lineal , ainsi que trois systèmes intermédiaires, également intéressants en eux-même : Scalar, Additive et λCA, chacun avec leurs preuves de préservation de type et de normalisation forte.





I am happy to announce that my thesis defence, accompanied of a QuAND meeting, will be held on September 23 at Grenoble. Here you are the programme, the venue and the thesis details.

PROGRAMME:
10h - 11h:
  Business meeting of the QuAND project (private)
11h15 - 12h:
  Seminar by Michele Pagani "Working for a theory of algebraic abstract reduction systems"
12h - 14h:
  Lunch
14h30 - 16h:
  Alejandro Díaz-Caro's thesis defence: "On vectorial typing"
16h:
  Drinks

VENUE:


Here is a map http://g.co/maps/rc8dc and some details:
From the train station, you can take the Tram B in direction "Plaine des sports", and take off at the stop "Bibliothèques universitaires".
The QuAND meeting will be held at the Aquarium room, and the defence at the lecture hall of the MJK building (Maison Jean Kuntzmann), same as the drinks afterwards.


DETAILS OF THE THESIS:

Title :
On vectorial typing
By:
Alejandro DÍAZ-CARO
Adviser:
Pablo ARRIGHI
Co-adviser:
Frédéric PROST

The defence will take place on Friday, September 23, 2011 at 2:30 pm in front of the following jury:

Rapporteurs:
Gilles DOWEK
Directeur de recherche - INRIA Centre Paris-Rocquencourt 
Thomas EHRHARD
Directeur de recherche CNRS - Laboratoire Preuves, Programmes et Systèmes 
Eduardo BONELLI
Profesor Asociado and Investigador Adjunto - Universidad Nacional de Quilmes et CONICET

Examinateurs:
Philippe JORRAND
Directeur de Recherche Émérite - CNRS
Laurent REGNIER
Professeur - Université de la Méditerranée
Lionel VAUX
Maitre de Conférences - Université de la Méditerranée
Michele PAGANI
Maitre de Conférences - Université de Paris Nord

Thesis adviser:
Pablo ARRIGHI
Maitre de Conférences - Université de Grenoble

Thesis 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.





Me es un placer anunciarles que mi defensa de tesis, acompañada de un encuentro QuAND, será el 23 de Setiembre en Grenoble. Aquí tienen el programa, las informaciones prácticas y los detalles de la tesis.

PROGRAMA:

10h - 11h:
  Encuentro de trabajo del proyecto QuAND (privado)
11h15 - 12h:
  Charla de Michele Pagani "Working for a theory of algebraic abstract reduction systems"
12h - 14h:
  Almuerzo
14h30 - 16h:
  Defensa de tesis de Alejandro Díaz-Caro: "Sobre el tipage vectorial"
16h:
  Brindis

INFORMACIÓN PRÁCTICA:

Aquí hay un mapa http://g.co/maps/rc8dc y algunos detalles:
Desde la estación de trenes, pueden tomar el Tram B en dirección "Plaine des sports", y bajarse en la parada "Bibliothèques universitaires".
El encuentro QuAND será en la sala Aquarium, y la defensa en el anfiteatro del edificio MJK (Maison Jean Kuntzmann), al igual que el brindis.

DETALLES DE LA TESIS:

Título:
Sobre el tipage vectorial
Por:
Alejandro DÍAZ-CARO
Director:
Pablo ARRIGHI
Co-director:
Frédéric PROST


La defensa se llevará a cabo el viernes 23 de Setiembre de 2011 a las 14:30hs delante del jurado compuesto por:

Rapporteurs:
Gilles DOWEK
Directeur de recherche - INRIA Centre Paris-Rocquencourt 
Thomas EHRHARD
Directeur de recherche CNRS - Laboratoire Preuves, Programmes et Systèmes 
Eduardo BONELLI
Profesor Asociado e Investigador Adjunto - Universidad Nacional de Quilmes et CONICET

Examinateurs:
Philippe JORRAND
Directeur de Recherche Émérite - CNRS
Laurent REGNIER
Professeur - Université de la Méditerranée
Lionel VAUX
Maitre de Conférences - Université de la Méditerranée
Michele PAGANI
Maitre de Conférences - Université de Paris Nord

Director de tesis:
Pablo ARRIGHI
Maitre de Conférences - Université de Grenoble

Resumen de la tesis
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.