Je suis chargé de recherche CNRS au sein du pôle PPS du laboratoire IRIF (UMR 8243) et membre de l'équipe
INRIA πr2.
Je suis actuellement responsable du GT Scalp (Structures formelles pour le CaLcul et les Preuves) au sein du GDR Informatique Mathématique et membre élu de la commission recherche de l'Université de Paris (élu de la liste Pari(s) d'une université plus humaine). En outre, je participe à diverses instances collectives de l'IRIF (je suis correspondant doctorant, membre du conseil de laboratoire et participe à la commission parité ainsi qu'à la commission locaux).
Aupravant, j'ai coordonné le projet ANR RAPIDO, été responsable pédagogique du Master 2 de mathématiques LMFI (Logique mathématique et fondements de l'informatique) et été pendant longtemps organisateur du séminaire PPS.
Mes recherches portent sur les liens entre théorie de la programmation et théorie de la démonstration. Plus spécifiquement, je m'intéresse:
- aux propriétés et structures de données infinitaires en logique et en programmation, notamment à la coinduction, aux logiques à points fixes et aux systèmes de types (co)inductifs ainsi qu'aux systèmes de preuves et de calculs infinitaires ou circulaires. Je m'intéresse notamment aux problématiques de productivité de ce cadre, ainsi qu'aux stratégies d'évaluation paresseuses permettant de manipuler des données infinies;
- à la théorie de la démonstration classique, intuitionniste et linéaire, notamment aux questions liées aux phénomènes de polarisation et de focalisation en logique ainsi qu'aux liens qu'entretiennent ces logiques;
- au lambda-calcul et à ses extensions classiques et infinitaires;
- à la notion d'interaction en logique et en programmation (Ludique, sémantique des jeux, etc.) et notamment à la sémantique des preuves et des programmes qui s'appuient sur cette notion d'interaction ainsi qu'aux réseaux de preuves de la logique linéaire;
- au contenu logique des opérateurs de contrôle des langages de programmation fonctionnels, notamment au contrôle délimité;
- à la recherche de preuve;
- aux stratégies d'évaluation des langages fonctionnels (appel par nom, appel par valeur, appel par nécessité) et notamment à l'utilisation des calculs des séquents pour étudier ces questions;
- à la formalisation de résultats de logique dans des assistants de preuve comme Coq;
- depuis peu, je m'intéresse également aux phénomènes probabilistes et quantiques dans une cadre logique et calculatoire.
Voici la liste des doctorants et post-doctorants que j'ai encadré:
- Kostia Chardonnet. Thèse débutée en novembre 2019, co-encadrée avec Benoît Valiron.
- Farzad Jafarrahmani. Thèse débutée en octobre 2019, co-encadrée avec Thomas Ehrhard.
- Luc Pélissier, post-doc de décembre 2018 à fin septembre 2019.
- Abhishek De. Thèse débutée en octobre 2018.
- Rémi Nollet. Thèse débutée en octobre 2016, co-encadrée avec Christine Tasson (soutenance prévue au premier semestre 2020).
- Andrew Polonsky, post-doc de janvier 2016 à fin 2017.
- Guilhem Jaber, post-doc de décembre 2015 à décembre 2016. Guilhem est maintenant maître de conférences à l'université de Nantes
- Amina Doumane. Thèse soutenue en juin 2017, co-encadrée avec David Baelde, thèse dirigée par Pierre-Louis Curien. Amina est maintenant chargée de recherche au CNRS.
- Pierre-Marie Pédrot. Thèse soutenue en septembre 2015, co-encadrée avec Hugo Herbelin. Pierre-Marie est maintenant chargé de recherche INRIA dans l'équipe Galinette.
Par ailleurs, j'ai encadré les stages (de niveau L3 au M2) de Kostia Chardonnet, Ikram Cherigui, Lucien David, Pablo Donato, Amina Doumane, Paul Downen, Paul Fermé, Fanny Hé, Simon Lunel et Luke Maurer, Rémi Nollet, Xavier Onfroy.
Je suis actuellement responsable du GT Scalp (Structures formelles pour le CaLcul et les Preuves) au sein du GDR Informatique Mathématique et membre élu de la commission recherche de l'Université de Paris (élu de la liste Pari(s) d'une université plus humaine). En outre, je participe à diverses instances collectives de l'IRIF (je suis correspondant doctorant, membre du conseil de laboratoire et participe à la commission parité ainsi qu'à la commission locaux).
Aupravant, j'ai coordonné le projet ANR RAPIDO, été responsable pédagogique du Master 2 de mathématiques LMFI (Logique mathématique et fondements de l'informatique) et été pendant longtemps organisateur du séminaire PPS.
Après avoir longtemps été responsable du Master 2 Logique mathématique et fondements de l'informatique (LMFI) de l'université Paris Diderot (avec René Cori, Martin Hils puis Boban Velickovic), je continue à y enseigner
le cours Outils classiques pour la correspondance preuves-programmes avec Christine Tasson. Auparavant, j'y ai enseigné
le Cours Fondamental de théorie de la démonstration ainsi que les cours d'orientation intitulés Outils classiques pour la correspondance preuves-programmes et Lambda-calcul et preuves (avec Thomas Ehrhard puis Christine Tasson) de l'université Paris Diderot. J'ai également pu intervenir ponctuellement dans le cadre de la section des étudiants empêchés de Paris Diderot (CP Fresnes et MA de Paris la Santé) ou dans la licence d'informatique de l'UFR d'informatique.
Le plus simple est le courrier électronique: prénom.nom@irif.fr ou le téléphone au 01.57.27.93.37.
Vous pouvez également utiliser le bon vieux courrier postal:
Alexis Saurin
Laboratoire PPS
Université Paris Diderot - Paris 7
Case 7014
75205 PARIS Cedex 13
Le laboratoire se trouve dans le nouveau bâtiment Sophie Germain de l'Université Paris-Diderot. Mon bureau est le 3040.
Pointeurs vers quelques collègues et amis chercheurs (maths, info, logique, sciences humaines):
David Baelde,
Adrien Deloro,
Etienne Duchesne,
Germain Faure,
Marco Gaboardi,
Aurélien Galateau,
Antonin Guilloux,
Stéphane Lengrand,
Assia Mahboubi,
Damiano Mazza,
Olivier Milhaud,
Joseph Najnudel,
Michele Pagani,
Magali Reghezza-Zitt,
Christine Tasson,
Pierre-Victor Tournier,
Noam Zeilberger, ...