Thematic team Pole Proofs, programs and systems Proofs and programs Leader Hugo Herbelin Research teams Our methodology is based on the Curry-Howard correspondence between proofs and programs, where rewriting plays a central role, describing both cut-elimination in proof theory and operational semantics of programs. The basic object is the lambda-calculus, which is a pure theory of functional programming and of its extensions: by type systems, linear or differential refinements, pattern-matching mechanisms, or various kinds of non-purely functional computational effects (nondeterministic or probabilistic choice, continuations, local or nonlocal internal states, etc.). We thus obtain formalisms that are interesting for their logical properties, giving for example a computational interpretation of standard concepts in logic (like the choice or reductio ad absurdum). We also get abstract representations of real programming languages, in a framework that is as implementation-independent as possible, that allows semantics analysis. Among these extensions, the calculus of inductive constructions is both a logic and a programming language, on which the Coq proof assistant is based. Members Name@PhoneOfficePositionPoleTeam Allioux Antoine @ 01 57 27 92 28 3034 Doctorant.e PPS pi.r2 , algebre , preuves Amadio Roberto @ 01 57 27 92 47 4020 Professeur.e PPS preuves , systemes Barenbaum Pablo @ 01 57 27 92 92 3026 Doctorant.e PPS algebre , preuves Batmalle Hadrien @ 01 57 27 92 43 3033 Doctorant.e PPS preuves Behr Nicolas @ 01 57 27 92 21 4029a Post-Doctorant.e PPS , ASD algebre , systemes , preuves , compsys Berline Chantal @ Membre associé.e PPS preuves Bernardi Giovanni @ 01 57 27 93 38 4026 Maître.sse de conférence PPS , ASV preuves , systemes , verif Blot Valentin @ Post-Doctorant.e PPS algebre , preuves Bucciarelli Antonio @ 01 57 27 94 33 3045 Maître.sse de conférence PPS algebre , preuves Cagne Pierre @ 01 57 27 92 92 3044 Doctorant.e avec mission d'enseignement PPS algebre , preuves Castagna Giuseppe @ 01 57 27 93 40 3039 Directeur.rice de recherche - CNRS PPS preuves , systemes Chouquet Jules @ 01 57 27 90 86 3032 Doctorant.e PPS preuves Crubillé Raphaëlle @ 01 57 27 92 43 3033 Doctorant.e PPS algebre , preuves Curien Pierre-Louis @ 01 57 27 92 23 3013 Directeur.rice de recherche - CNRS PPS algebre , pi.r2 , preuves Ehrhard Thomas @ 01 57 27 92 17 4014a Directeur.rice de recherche - CNRS PPS algebre , preuves , systemes Faggian Claudia @ 01 57 27 92 55 3049 Chargé.e de recherche - CNRS PPS preuves , systemes , algebre Finster Eric @ 01 57 27 94 30 3018 Post-Doctorant.e PPS pi.r2 , algebre , systemes , preuves Galal Zeinab @ 01 57 27 90 86 3032 Doctorant.e PPS algebre , preuves Girka Thibaut @ 01 57 27 92 43 3033 Doctorant.e PPS pi.r2 , preuves , systemes Hamdaoui Yann @ 01 57 27 92 92 3026 Doctorant.e PPS preuves , systemes Herbelin Hugo @ 01 57 27 90 87 3029 Directeur.rice de recherche - INRIA PPS algebre , pi.r2 , preuves , systemes Ho Thanh Cédric @ 3032 Doctorant.e avec mission d'enseignement PPS pi.r2 , algebre , preuves Husson Adrien @ 01 57 27 92 22 3035 Doctorant.e PPS , ASD systemes , preuves , compsys Jacq Clément @ 01 57 27 92 92 3026 Doctorant.e avec mission d'enseignement PPS algebre , preuves Joly Thierry @ 01 57 27 90 88 3007 Maître.sse de conférence PPS preuves Kasterovic Simona @ 3055 Doctorant.e PPS preuves Kerjean Marie @ 01 57 27 94 16 3044 Doctorant.e avec mission d'enseignement PPS algebre , preuves Kesner Delia @ 01 57 27 92 38 3020 Professeur.e PPS algebre , preuves Krivine Jean-Louis @ 01 57 27 92 39 3008 Professeur.e émérite PPS algebre , preuves Krivine Jean @ 01 57 27 93 38 4026 Chargé.e de recherche - CNRS ASD , PPS compsys , preuves , systemes Lanvin Victor @ 01 57 27 92 22 3035 Doctorant.e PPS preuves , systemes Leena-Subramaniam Chaitanya @ 01 57 27 92 28 3034 Doctorant.e ASV , PPS automates , algebre , preuves Legrandgérard Yves @ 01 57 27 92 57 3057 Informaticien.ne PPS systemes , preuves Leivant Daniel @ Membre associé.e PPS algebre , preuves Letouzey Pierre @ 01 57 27 90 84 3028 Maître.sse de conférence PPS pi.r2 , preuves , systemes Leventis Thomas @ ATER PPS preuves Lévy Jean-Jacques @ 01 57 27 92 68 3009 Directeur.rice de recherche émérite - INRIA PPS pi.r2 , preuves , systemes Mangin Cyprien @ 01 57 27 92 28 3034 Doctorant.e PPS algebre , pi.r2 , preuves , systemes Melliès Paul-André @ 01 57 27 92 48 3023 Chargé.e de recherche - CNRS PPS , ASV algebre , automates , preuves Nollet Remi @ 01 57 27 92 92 3026 Doctorant.e avec mission d'enseignement PPS algebre , preuves Onfroy Xavier @ 3018 Stagiaire PPS systemes , preuves Osmond Axel @ 01 57 27 94 56 4060 Doctorant.e ASV , PPS automates , algebre , preuves Padovani Vincent @ 01 57 27 93 39 3045 Maître.sse de conférence PPS preuves Pagani Michele @ 01 57 27 92 56 4015 Professeur.e PPS algebre , preuves Parigot Michel @ 01 57 27 92 51 3047 Chargé.e de recherche - CNRS PPS preuves Petrucciani Tommaso @ 01 57 27 92 22 3035 Doctorant.e PPS preuves , systemes 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 Rozière Paul @ 01 57 27 92 57 3057 Maître.sse de conférence PPS 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 Stefanesco Leo @ 01 57 27 92 92 3026 Doctorant.e avec mission d'enseignement PPS algebre , preuves Tasson Christine @ 01 57 27 93 37 3040 Maître.sse de conférence PPS algebre , preuves , systemes Valiron Benoit @ Membre associé.e PPS algebre , preuves , systemes 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