INRIA project-team


Leader


External website

Research themes

The team $\pi r^2$ is an INRIA, Université Paris-Diderot — Paris 7 and CNRS joint project-team, inside the PPS team of the IRIF. It covers three research topics:

  • a fundamental research around the correspondence between proofs and programs,
  • a theoretical research around the formalism that underlies the Coq proof assistant,
  • an implementation field with the development of Coq, especially in the view of Coq as a dependently-typed programming language.

Research themes:

  • Crossed-fertilisation of proof theory and program theory
    The syntactic correspondence between proofs and programs (so-called Curry-Howard correspondence) irrigated logic and computer science in the last 30 years. In the last 15 years, new achievements have been obtained (discovery of a relation between logical reasoning by contradiction and control operators; between the formalism known as “sequent calculus” and the structures used in abstract evaluation machines, relevance of side effects in computing with the axiom of choice, …). One of the objectives of $\pi r^2$ is to explore the consequences and foundations of these recent progresses, especially by studying the logical content of the notion of continuation delimiters introduced in functional programming and by studying the relations between the operations of reflection and reification in programming and the notions of soundness and completeness in logic.
  • Study of type theory and of the Calculus of Inductive Constructions seen as programming languages
    The Calculus of Inductive Constructions is the name of the formalism underlying the Coq proof assistant. The Calculus of Inductive Constructions derives from Martin-Löf's type theory and is both an expressive logical formalism (comparable in strength to set theory) and a strongly-typed functional programming language (a kind of formalism classified as “type theory”). The Calculus of Inductive Constructions is a rather young formalism about which several questions of a technical nature are open. One of the objectives of $\pi r^2$ is to explore some of these questions: a native treatment of so-called “inversion” constraints with application to the typing of the pattern-matching programming construct in presence of “rich” types, support for a syntactic form of extensionality (so-called “eta-conversion”) with applications to the design of unification and type-inference algorithms in the presence of rich types.
  • Development of the Coq system, especially as a dependently-typed programming language
    The Coq proof assistant offers an environment for semi-interactive development of proofs in an expressive logic build on top of a strongly-typed programming languages. Jointly developed by several teams at INRIA and outside INRIA, Coq is equally used for the formalisation of mathematics and the certification of properties of programs. Natively equipped with dependent types, Coq has a role to play as a richly-typed programming language. Some objectives of $\pi r^2$ here are the development of certified programming libraries, the certification of the extraction process from Coq programs to functional programming languages such as OCaml, the development of new proof methods (so-called “tactics”). The $\pi r^2$ team also develops Pangolin which is a tool dedicated to the certification of functional programs.


Members

Name@PhoneOfficePositionPoleTeam
Allioux Antoine @ 01 57 27 92 28 3034 Doctorant.e PPS pi.r2 , algebre , preuves
Curien Pierre-Louis @ 01 57 27 92 23 3013 Directeur.rice de recherche - CNRS PPS algebre , pi.r2 , preuves
Finster Eric @ 01 57 27 94 30 3018 Post-Doctorant.e PPS pi.r2 , algebre , systemes , preuves
Girka Thibaut @ 01 57 27 92 43 3033 Doctorant.e PPS pi.r2 , preuves , systemes
Guiraud Yves @ 01 57 27 94 29 3012 Chargé.e de recherche - INRIA PPS algebre , pi.r2
Herbelin Hugo @ 01 57 27 90 87 3029 Directeur.rice de recherche - INRIA PPS algebre , pi.r2 , preuves , systemes
Ho Thanh Cédric @ 01 57 27 90 86 3032 Doctorant.e avec mission d'enseignement PPS pi.r2 , algebre , preuves
Letouzey Pierre @ 01 57 27 90 84 3028 Maître.sse de conférence PPS pi.r2 , preuves , systemes
Lévy Jean-Jacques @ 01 57 27 92 68 3009 Directeur.rice de recherche émérite - INRIA PPS pi.r2 , preuves , systemes
Malbos Philippe @ 01 57 27 94 29 3012 Membre associé.e PPS pi.r2 , algebre
Mangin Cyprien @ 01 57 27 92 28 3034 Doctorant.e PPS algebre , pi.r2 , preuves , systemes
Mimram Samuel @ Membre associé.e PPS pi.r2 , algebre
Régis-Gianas Yann @ 01 57 27 90 84 3028 Maître.sse de conférence PPS pi.r2 , preuves , systemes
Rivas Exequiel @ 01 57 27 94 30 3018 Post-Doctorant.e PPS pi.r2 , algebre , systemes , preuves
Saurin Alexis @ 01 57 27 93 37 3040 Chargé.e de recherche - CNRS PPS algebre , pi.r2 , preuves , systemes
Sozeau Matthieu @ 01 57 27 94 15 3019 Chargé.e de recherche - INRIA PPS algebre , pi.r2 , preuves , systemes
Spiwack Arnaud @ Membre associé.e PPS pi.r2 , algebre , preuves
Zimmermann Theo @ 01 57 27 92 28 3034 Doctorant.e PPS pi.r2 , systemes , preuves
de Rauglaudre Daniel @ 01 57 27 90 86 3030 Informaticien.ne PPS pi.r2 , preuves , systemes