The team Proofs, Programs and Systems (PPS) of IRIF brings together researchers and students with various scientific backgrounds (in computer science and mathematics) to work on the theme of the foundations and practice of programming languages and distributed systems. PPS also develops methods and tools for modelling biological systems, and new methods for developing and maintaining systems in a free software setting. Last, PPS is a major actor in the realm of proof assistants.

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.

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

Former webpage (PPS laboratory)