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.
| Name | @ | Phone | Office | Position | Pole | Team |
|---|---|---|---|---|---|---|
| Amadio Roberto | @ | 01 57 27 92 47 | 4020 | Professor | PPS | systemes , preuves |
| Baudart Guillaume | @ | 4026 | Research Scientist - INRIA ISFP | PPS | systemes , preuves , picube | |
| Behr Nicolas | @ | 01 57 27 90 85 | 3030 | Research Scientist - CNRS | PPS | algebre , preuves |
| Bernardi Giovanni | @ | 01 57 27 93 38 | 4021 | Associate Professor | ASV , PPS | verif , systemes , preuves |
| Bucciarelli Antonio | @ | 01 57 27 94 33 | 3045 | Associate Professor | PPS | algebre , preuves |
| Castagna Giuseppe | @ | 01 57 27 93 40 | 3039 | Senior Research Scientist - CNRS | PPS | preuves , systemes |
| Curien Pierre-Louis | @ | 01 57 27 92 23 | 3013 | Senior Research Scientist Emeritus - CNRS | PPS | picube , algebre , preuves |
| Douteau Sylvain | @ | 3030 | Associate Professor | PPS | algebre , preuves | |
| Ehrhard Thomas | @ | 01 57 27 92 17 | 4014a | Senior Research Scientist - CNRS | PPS | algebre , systemes , preuves , picube |
| Faggian Claudia | @ | 01 57 27 90 86 | 3032 | Research Scientist - CNRS | PPS | algebre , preuves |
| Férée Hugo | @ | 01 57 27 94 05 | 4011 | Associate Professor | PPS | systemes , preuves |
| Geoffroy Guillaume | @ | 01 57 27 94 15 | 3019 | Associate Professor | PPS | algebre , preuves |
| Guatto Adrien | @ | 01 57 27 94 15 | 3019 | Associate Professor | PPS | algebre , systemes , preuves |
| Herbelin Hugo | @ | 01 57 27 90 87 | 3029 | Senior Research Scientist - INRIA | PPS | algebre , picube , preuves , systemes |
| Joly Thierry | @ | 01 57 27 92 55 | 3049 | Associate Professor | PPS | preuves |
| Kesner Delia | @ | 01 57 27 92 38 | 3020 | Professor | PPS | algebre , preuves |
| Krivine Jean-Louis | @ | 01 57 27 92 39 | 3008 | Professor Emeritus | PPS | algebre , preuves |
| Letouzey Pierre | @ | 01 57 27 93 37 | 3040 | Associate Professor | PPS | picube , systemes , preuves |
| Lévy Jean-Jacques | @ | 01 57 27 92 68 | 3009 | Senior Research Scientist Emeritus - INRIA | PPS | systemes , preuves , picube |
| Manzonetto Giulio | @ | 01 57 27 93 54 | 4015 | Professor | PPS | algebre , preuves |
| Melliès Paul-André | @ | 01 57 27 92 48 | 3023 | Senior Research Scientist - CNRS | ASV , PPS | automates , algebre , preuves , picube |
| Padovani Vincent | @ | 01 57 27 93 39 | 3045 | Associate Professor | PPS | preuves |
| Rozière Paul | @ | 01 57 27 92 57 | 3057 | Pensioner - MCF Université Paris Cité | PPS | preuves |
| Saurin Alexis | @ | 01 57 27 93 37 | 3040 | Research Scientist - CNRS | PPS | algebre , systemes , preuves , picube |
| Scherer Gabriel | @ | 4032 | Research Scientist - INRIA | PPS | algebre , systemes , preuves , picube |