Thematic team


Leader


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

NamePhoneOfficePositionMail
Amadio Roberto 01 57 27 92 47 4020 Professeur.e Mail
Barenbaum Pablo 01 57 27 92 92 3026 Doctorant.e Mail
Batmalle Hadrien 01 57 27 92 43 3033 Doctorant.e Mail
Behr Nicolas 4029a Post-Doctorant.e Mail
Berline Chantal Membre associé.e Mail
Bernardi Giovanni 01 57 27 93 38 4026 Maître.sse de conférence Mail
Bucciarelli Antonio 01 57 27 94 33 3045 Maître.sse de conférence Mail
Cagne Pierre 01 57 27 92 92 3026 Doctorant.e avec mission d'enseignement Mail
Castagna Giuseppe 01 57 27 93 40 3039 Directeur.rice de recherche - CNRS Mail
Chouquet Jules 3032 Doctorant.e Mail
Claret Guillaume 01 57 27 92 28 3034 Doctorant.e Mail
Crubillé Raphaëlle 01 57 27 92 43 3033 Doctorant.e Mail
Curien Pierre-Louis 01 57 27 92 23 3013 Directeur.rice de recherche - CNRS Mail
Ehrhard Thomas 01 57 27 92 17 4014a Directeur.rice de recherche - CNRS Mail
Faggian Claudia 01 57 27 92 55 3049 Chargé.e de recherche - CNRS Mail
Favro Giordano 01 57 27 90 86 3032 Doctorant.e Mail
Finster Eric Post-Doctorant.e Mail
Galal Zeinab Doctorant.e Mail
Girka Thibaut 01 57 27 92 43 3033 Doctorant.e Mail
Hamdaoui Yann 01 57 27 92 92 3026 Doctorant.e Mail
Herbelin Hugo 01 57 27 90 87 3029 Directeur.rice de recherche - INRIA Mail
Ho-Thanh Cedric 3032 Doctorant.e avec mission d'enseignement Mail
Husson Adrien 01 57 27 57 27 3044 Doctorant.e Mail
Jaber Guilhem 01 57 27 94 30 3018 Post-Doctorant.e Mail
Jacq Clément 01 57 27 92 92 3026 Doctorant.e avec mission d'enseignement Mail
Joly Thierry 01 57 27 90 88 3007 Maître.sse de conférence Mail
Kerjean Marie 01 57 27 94 16 3044 Doctorant.e avec mission d'enseignement Mail
Kesner Delia 01 57 27 92 38 3025 Professeur.e Mail
Krivine Jean-Louis 01 57 27 92 39 3008 Professeur.e émérite Mail
Krivine Jean 01 57 27 93 38 4026 Chargé.e de recherche - CNRS Mail
Lanvin Victor 01 57 27 92 22 3035 Doctorant.e Mail
Leena-Subramaniam Chaitanya 3034 Doctorant.e Mail
Leivant Daniel Membre associé.e Mail
Letouzey Pierre 01 57 27 90 84 3028 Maître.sse de conférence Mail
Lévy Jean-Jacques 01 57 27 92 68 3009 Directeur.rice de recherche émérite - INRIA Mail
Mangin Cyprien 01 57 27 92 28 3034 Doctorant.e Mail
Melliès Paul-Andre 01 57 27 92 48 3023 Chargé.e de recherche - CNRS Mail
Miquey Étienne 01 57 27 92 22 3035 Doctorant.e Mail
Nollet Remi 3026 Doctorant.e Mail
Osmond Axel 4060 Doctorant.e Mail
Padovani Vincent 01 57 27 93 39 3045 Maître.sse de conférence Mail
Pagani Michele 01 57 27 92 56 4015 Professeur.e Mail
Parigot Michel 01 57 27 92 51 3047 Chargé.e de recherche - CNRS Mail
Petrucciani Tommaso 01 57 27 92 22 3035 Doctorant.e Mail
Régis-Gianas Yann 01 57 27 90 84 3028 Maître.sse de conférence Mail
Rozière Paul 01 57 27 92 57 3057 Maître.sse de conférence Mail
Saurin Alexis 01 57 27 93 37 3040 Chargé.e de recherche - CNRS Mail
Sozeau Matthieu 01 57 27 94 15 3019 Chargé.e de recherche - INRIA Mail
Stefanesco Leo 3026 Doctorant.e Mail
Tasson Christine 01 57 27 93 37 3040 Maître.sse de conférence Mail
Valiron Benoit 3018 Membre associé.e Mail
Vial Pierre 01 57 27 92 92 3026 Doctorant.e Mail
Zimmermann Theo 01 57 27 92 28 3034 Doctorant.e Mail
de Rauglaudre Daniel 01 57 27 90 86 3030 Informaticien.ne Mail