Équipe-projet Inria Pôle Preuves, programmes et systèmes $\pi r^2$ (Inria) Responsable Alexis Saurin Page web externe https://www.inria.fr/equipes/pi.r2 Thèmes de recherche L'équipe $\pi r^2$ est une équipe-projet commune à l'INRIA, à l'Université Paris-Diderot et au CNRS, au sein de l'équipe Preuves, Programmes et Systèmes de l'IRIF. Elle couvre trois champs de recherche : un champ de recherche fondamentale autour de la correspondance entre preuves et programmes ; un champ de recherche théorique autour du formalisme sur lequel repose l'environnement de développement de preuves et de programmes Coq ; un champ implémentatoire avec le développement du logiciel Coq, notamment dans ses aspects langage de programmation à types « riches ». Axes de recherche : Fertilisation croisée entre la théorie de la démonstration et la théorie des programmes. La correspondance syntaxique entre preuves et programmes, dite correspondance de Curry-Howard a été au cours des 30 dernières années un formidable moteur de la recherche tant pour la logique (la plupart des axiomes logiques sont calculatoires : par exemple, la preuve d'un énoncé existentiel est un procédé de calcul qui ultimement exhibe un témoin de cette existence) que pour la programmation (les types de données sont des formules spécifiant les propriétés des programmes et ces types peuvent être des formules arbitrairement complexes). Dans les 15 dernières années, de nouvelles étapes ont été franchies (mise en évidence d'une connexion entre raisonnement par l'absurde et opérateurs de contrôle, entre le formalisme logique dit « du calcul des séquents » et les structures des machines d'évaluation abstraites, rôle des effets de bord dans l'interprétation calculatoire de l'axiome du choix, …). L'un des objectifs de $\pi r^2$ est alors d'explorer les conséquences et fondements de ces dernières avancées, notamment en étudiant le contenu logique des délimiteurs de continuations issus de la programmation fonctionnelle, et en étudiant les relations entre les mécanismes de réflexion/réification en programmation et de correction/complétude en logique. Étude du Calcul des Constructions Inductives et de la théorie des types dans leurs aspects « langage de programmation ». Le Calcul des Constructions Inductives est le nom du formalisme logique sur lequel repose Coq. Ce formalisme, qui dérive de la théorie des types de Martin-Löf, est à la fois un formalisme logique expressif (comparable en force à la théorie des ensembles) et un langage de programmation fonctionnelle fortement typé (type de formalisme que l'on range dans la famille des « théories des types »). Le Calcul des Constructions Inductives est un formalisme relativement jeune au sujet duquel plusieurs questions restent ouvertes. L'un des objectifs de $\pi r^2$ est d'explorer quelques unes de ces questions, certaines étant d'un abord assez technique : traitement plus primitif des contraintes dites d'« inversion » lors des constructions par cas avec application au typage de la programmation par filtrage en présence de types « riches », prise en compte d'une forme syntaxique d'extensionnalité des fonctions (« éta-conversion ») avec applications à la conception d'algorithmes d'unification et d'inférence de type en présence de types riches. Développement du logiciel Coq, notamment dans ses aspects langage de programmation. Le logiciel Coq est un outil de développement semi-interactif de preuves dans une logique expressive bâtie autour d'un langage de programmation fonctionnelle fortement typé. Développé conjointement par plusieurs équipes INRIA et hors INRIA, Coq est utilisé tant pour la formalisation des mathématiques que pour la certification de propriétés de programmes. Naturellemment doté de types « dépendants », Coq a une carte à jouer comme langage de programmation à type « riches ». Un des objectifs de $\pi r^2$ dans ce cadre est le développement de bibliothèques de programmation certifiés, la certification du processus d'« extraction » de programme Coq vers des langages fonctionnels comme OCaml, ainsi que le développement de nouvelles méthodes de preuves (des « tactiques ») pour Coq. L'équipe πr² développe aussi Pangolin qui est un outil spécifique de certification de programmes fonctionnels. Permanents en poste à l'IRIF Nom@TéléphoneBureauFonctionPôleÉquipe Curien Pierre-Louis @ 01 57 27 92 23 3013 Directeur.rice de recherche émérite - CNRS PPS pi.r2 , algebre , preuves De Rauglaudre Daniel @ 01 57 27 90 86 3030 Ingénieur de recherche PPS pi.r2 , systemes , preuves Herbelin Hugo @ 01 57 27 90 87 3029 Directeur.rice de recherche - INRIA PPS algebre , pi.r2 , preuves , systemes Letouzey Pierre @ 01 57 27 93 37 3040 Maître.sse de conférences PPS pi.r2 , systemes , preuves Lévy Jean-Jacques @ 01 57 27 92 68 3009 Directeur.rice de recherche émérite - INRIA PPS pi.r2 , preuves , systemes Martinez Thierry @ 3030 Informaticien.ne - INRIA PPS pi.r2 , preuves Saurin Alexis @ 01 57 27 93 37 3040 Chargé.e de recherche - CNRS PPS pi.r2 , algebre , systemes , preuves Permanents en poste hors de l'IRIF Nom@TéléphoneBureauFonctionSiteÉquipe Mathurin Anne @ 01 80 49 40 37 A118 Assistante de l'Équipe CRI Paris pi.r2 Non-permanents Nom@TéléphoneBureauFonctionPôleÉquipe Allioux Antoine @ 01 57 27 92 28 3034 Doctorant.e PPS pi.r2 , algebre , preuves Blazy Vincent @ 3044 Doctorant.e PPS pi.r2 , algebre , preuves Castro Felix @ 3026 Doctorant.e PPS pi.r2 , algebre , systemes , preuves Chanavat Mathieu @ Stagiaire pi.r2 Chardonnet Kostia @ 3044 Doctorant.e PPS pi.r2 , preuves De Abhishek @ 01 57 27 92 92 3026 Doctorant.e PPS pi.r2 , algebre , preuves Djuric Alen @ 3033 Doctorant.e PPS pi.r2 , algebre Gallego Emilio @ 01 57 27 92 24 4030 Starting research position - INRIA PPS pi.r2 , algebre , systemes , preuves Gonzalez Colin @ 3044 Doctorant.e PPS pi.r2 , systemes Jafar-Rhamani Farzad @ 01 57 27 92 92 3026 Doctorant.e PPS pi.r2 , algebre , systemes , preuves Moeneclaey Hugo @ 3034 Doctorant.e PPS pi.r2 , algebre , systemes , preuves Moreau Vincent @ 4033 Doctorant.e ASV , PPS automates , pi.r2 , algebre Spiwack Arnaud @ Membre associé.e - EURL Tweag PPS pi.r2 , algebre , preuves Zimmermann Theo @ 01 57 27 94 15 3019 Post-Doctorant.e - Ingénieur R&D Inria PPS pi.r2 , systemes , preuves Informations pratiques Partir en mission à l'INRIA Rapport d'activité 2020 de l'équipe Rapport d'activité 2020 de l'équipe (pdf)