English version

Lionel Rieg

De septembre 2014 à août 2016, je suis ATER au Collège de France avec Gérard Berry.
Auparavant, j'ai été:

Travaux de thèse

La page de ma thèse.

Le thème de recherche de ma thèse est la réalisabilité classique, et plus particulièrement le contenu calculatoire que l'on peut donner au forcing dans ce cadre. J'ai aussi travaillé sur l'introduction des nombres réels dans la KAM (Krivine Abstract Machine).

J'ai formalisé une preuve (classique) du théorème de Herbrand dans l'assistant de preuves Coq qui, après extraction, fournit un algorithme certifié en λc-calcul de calcul d'arbres de Herbrand.
Ici se trouve la version actualisée qui utilise les typeclasses et simplifie la preuve. Elle a été testée pour Coq v. trunk (14464). Le dossier contient également un makefile et un fichier d'optimisation des réalisateurs lors de l'extraction par kextraction.
Depuis, j'en ai obtenu une preuve par forcing qui se passe du théorème de l'éventail (fan theorem) et dont on peut extraire un réalisateur à travers la traduction du forcing en réalisabilité classique. L'ingrédient crucial de cette preuve est l'ajout d'un réel de Cohen.
Ce travail a donnée lieu a une publication à CSL 2013 disponible librement ici.

J'ai également formalisé la réalisabilité classique en Coq. La machine sous-jacente est une version de la KAM avec environnement à laquelle j'ai ajouté diverses extensions comme les entiers et rationnels primitifs, les réels (en partie), ou le non-déterminisme. Elle a été testée avec Coq v. trunk (14850) car les versions ultérieures ne supportent plus l'extracteur classique (kextraction). En abandonnant l'extraction classique, elle compile actuellement avec Coq v.8.4pl3 ainsi que la version trunk.

Depuis la fin de ma thèse, je me suis d'avantage intéressé aux assistants de preuve et à la certification de programmes, en calcul distribué et en programmation synchrone.

Preuves formelles sur les essaims de robots

Le projet Pactole cherche un formaliser des résultats sur les essaims de robots dans un cadre unifié. On peut y faire à la fois des preuve d'impossibilité (par exemple l'impossibilité du rassemblement sur une droite réelle) et des preuves d'algorithmes (rassemblement dans le plan).

Preuve formelle de la compilation de langages synchrones

Actuellement, je formalise la compilation d'Esterel vers les circuits, l'objectif à terme étant d'extraire le compilateur, à la manière de CompCert.
Un autre projet auquel je participe, Vélus, s'attaque à la formalisation de la compilation de Lustre vers du code impératif, en particulier vers le langage intermédiaire Clight de CompCert.

Voici quelques exposés que j'ai donnés.

La liste de mes publications.

Me contacter

Enseignements

Année 2008-2009
Année 2010-2011
Année 2011-2012
Année 2012-2013
Année 2013-2014
Années 2014-2015 et 2015-2016