Presentation

The team πr² is a joint INRIA project-team with the CNRS and the Université Paris-Diderot – Paris 7, led by Pierre-Louis Curien. It belongs to the INRIA Paris-Rocquencourt research center and it is a part of the PPS team.

The team πr² covers three research topics:

• a fundamental research around the correspondence between proofs and programs,

• a theoretical research around the formalism that underlies the Coq proof assistant,

• an implementation field with the development of Coq, especially in the view of Coq as a dependently-typed programming language.

News

• Spring 2014 – The thematic trimester Semantics of proofs and certified mathematics of the Institut Henri Poincaré is organised from April 22 to July 11 by Pierre-Louis Curien, Hugo Herbelin and Paul-André Melliès.

• April 2014 – Coq receives the Software System Award 2013 from the ACM.

• June 2013 – Coq receives the Programming Languages Software Award 2013 from the ACM SIGPLAN, attributed during the POPL 2014 congress.

Contact

Scientific leader
Pierre-Louis Curien
01.57.27.92.23 Secretary
Lindsay Polienor
01.39.63.78.90 Mail address
Laboratoire PPS
Université Paris-Diderot
Case 7014
75205 Paris Cedex 13 Physical address
Sophie Germain building
8 place FM/13
(Av. de France / Rue A.-Domon-et-L.-Duquet)
75013 Paris