J'ai le plaisir de vous inviter à ma soutenance de thèse qui se déroulera dans très exactement une semaine:
ainsi qu'au pot qui suivra.

Titre de la thèse: Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique)
La version préliminaire de la thèse est disponible à http://www.lix.polytechnique.fr/~saurin/Recherche/These

Résumé: Théorie de la démonstration et calcul entretiennent des liens très profonds, notamment par le biais de deux paradigmes de programmation: la programmation fonctionnelle et la programmation logique. La thèse porte sur les fondements logiques de ces deux paradigmes de programmation: la recherche de preuve et l'élimination des coupures.
Plus précisément, nous proposons une série de développements concernant la compréhension, en logique, de constructions des langages fonctionnels et logiques permettant de contrôler l'exécution du programme:
-- Du côté programmation fonctionnelle, nous développons la méta-théorie du Lambda-mu-calcul, une extension du lambda-mu-calcul de Parigot que nous avons introduite pour résoudre le problème de la non-séparation du lambda-mu-calcul.
-- Du côté programmation logique, nous proposons un système de recherche de preuve par interaction fondé sur la Ludique de Girard. Il s'agit d'une recherche de preuve par élimination des coupures.
-- Enfin, nous étudions la propriété de focalisation de la logique linéaire, propriété due à Andreoli, résultat fondamental en programmation logique linéaire et en Ludique.

Le Jury sera composé de:
Pierre-Louis Curien
Olivier Danvy
François Fages
Jean-Yves Girard
Olivier Laurent
Dale Miller
Luke Ong
Simona Ronchi della Rocca

Pour venir à l'Ecole Polytechnique:
http://www.polytechnique.fr/campus/campus_plans.php
http://www.polytechnique.fr/images/campus/acceslozere.jpg
http://www.polytechnique.fr/images/campus/plan_ecole.pdf
(l'amphi Arago porte le numéro 14 dans le plan ci-dessus)


--
Alexis Saurin