The PPS laboratory (Proofs, Programs and Systems) is a joint lab of the CNRS (Centre National de la Recherche Scientifique) and the Université Paris-Diderot. It belongs to the INS2I (Institut des Sciences Informatiques et de leurs Interactions) and the INSMI (Institut des Sciences Mathématiques et de leurs Interactions) of the CNRS. It additionally runs the joint project πr² with INRIA and plays a crucial role, in collaboration with INRIA and UPMC, in the "Initiative de Recherche et Innovation sur l'Informatique du Logiciel Libre" (Research and Innovation in Free Software).

The lab brings together researchers and students from different cultures (computer science and mathematical logic) to work on the theme of the foundations and practice of programming languages and distributed systems. In this perspective, it researches new methods for there development and maintenance of large open source projects. It is also a major player in the area of computer-assisted theorem proving.

Our research agenda is founded on the idea that mathematical logic (particularly proof theory) and related areas – such as category theory, homotopy, homology and probability – have an important role to play in the elucidation of the meaning, and reliability, of programs. Conversely, we also consider that computer science can be – as physics has long been and still remains – a source of renewal for logic and other mathematical disciplines.