Proofs and programs

Head

Research themes

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).

Seminar and working groups

Proofs, programs and systems
Semantics
Type theory and realisability

Permanent members

Search:

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

Non-permanent members

Search:

Name	@	Phone	Office	Position	Pole	Team
Arambillete Santiago	@		3033	PhD Student	PPS	preuves
Arrial Victor	@		3018	PhD Student	PPS	preuves
Barszezak Yoann	@			Teaching and Research Assistant	PPS	preuves , algebre
Bauer Esaie	@		3028	PhD Student	PPS	preuves , picube
Catz Manuel	@		4055	PhD Student	PPS	preuves
Cerda Remy	@		3057	Post-Doc	PPS	algebre , preuves
Cherradi El-Mehdi	@		4054	PhD Student	ASV , PPS	automates , algebre , preuves
De Faveri Arturo	@		4033	PhD Student	PPS	algebre , preuves
Di Donna Raffaele	@		3010	PhD Student	PPS	algebre , preuves
Gallego Emilio	@	01 57 27 92 24	4030	Starting research position - INRIA	PPS	picube , algebre , preuves , programmes
Giusti Giulia	@		4055	PhD Student	PPS	algebre , preuves
Huang Xuejing	@		3018	Post-Doc	PPS	programmes , preuves
Jafar-Rhamani Farzad	@	01 57 27 92 92	3026	Post-Doc	PPS	algebre , programmes , preuves , picube
Jubert Moana	@		3034	PhD Student	PPS	picube , algebre , preuves
Kirst Dominik	@		4053	Post-Doc	PPS	preuves , picube , programmes
Lancelot Adrienne	@		3026	PhD Student	PPS	preuves
Laurent Mickael	@		3033	PhD Student	PPS	programmes , preuves
Manara Giulia	@		3014	PhD Student	PPS	preuves
Mangel Eleonore	@			PhD Student	PPS	preuves
Martinez Thierry	@	01 57 27 90 87	3029	Research ingenior - INRIA	PPS	preuves , picube
Marzaioli Miriam	@		4055	PhD Student	PPS	algebre , preuves
Mathieu Adrien	@			Intern	PPS	preuves , picube , programmes
Milicich Mariana	@		3026	PhD Student	PPS	algebre , preuves
Pasquale Valentin	@			PhD Student	PPS	algebre , preuves
Ramos Miguel	@		3033	PhD Student	PPS	algebre , preuves
Reboullet Sarah	@		3034	PhD Student	PPS	preuves , picube
Salibra Antonino	@			Associated Member	PPS	algebre , preuves
Vanoni Gabriele	@		3018	Post-Doc	PPS	algebre , preuves
Vienot Ada	@		3044	PhD Student	PPS	algebre , programmes , preuves