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, including nondeterministic, probabilistic or quantum 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. We also study the theoretical foundations for probabilistic programming languages (here), and for quantum programming languages (here).
| Name | @ | Phone | Office | Position | Pole | Team |
|---|---|---|---|---|---|---|
| Amadio Roberto | @ | 01 57 27 92 47 | 4020 | Professor | PPS | preuves |
| Baudart Guillaume | @ | 4026 | Research Scientist - INRIA ISFP | PPS | picube , preuves , programmes | |
| Behr Nicolas | @ | 01 57 27 90 85 | 3030 | Research Scientist - CNRS | PPS | algebre , preuves |
| Bernardi Giovanni | @ | 01 57 27 93 38 | 4021 | Associate Professor | PPS , ASV | preuves , verif , programmes |
| 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 , programmes |
| 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 , programmes , 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 | programmes , 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 , programmes , preuves |
| Herbelin Hugo | @ | 01 57 27 90 87 | 3029 | Senior Research Scientist - INRIA | PPS | algebre , picube , preuves , programmes |
| 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 , programmes , preuves |
| Lévy Jean-Jacques | @ | 01 57 27 92 68 | 4032 | Senior Research Scientist Emeritus - INRIA | PPS | preuves , picube , programmes |
| 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 |
| Narboux Julien | @ | 01 57 27 92 58 | 3022 | Associate Professor | PPS | programmes , preuves |
| Padovani Vincent | @ | 01 57 27 93 39 | 3045 | Associate Professor | PPS | preuves |
| Rozière Paul | @ | Pensioner - MCF Université Paris Cité | PPS | preuves | ||
| Saurin Alexis | @ | 01 57 27 93 37 | 3040 | Research Scientist - CNRS | PPS | algebre , programmes , preuves , picube |
| Scherer Gabriel | @ | 4032 | Research Scientist - INRIA | PPS | algebre , programmes , preuves , picube |