The Barcelona Group on Proof Theory agglomerates the most active exponents that work on areas in or related to proof theory in the general Barcelona area. The group comprises various theoretical lines of research as well as practical and applied lines of research.

Theoretical research involves proof theoretic analysis of formal mathematical theories in general. Apart from studies on interpretability and related logics, a central theme is so-called $\Pi^0_1$ ordinal analysis. Other interests concern proof complexity and informative proof systems.

The applied proof theory involves generation of verified software using proof assistants based on dependent polymorphic type theory and the Curry-Howard isomorphism.

Apart from the core members, the group includes some prominent external researchers related to our project and activities. The group counts with numerous official projects funded through Catalan, Spanish and European funding alike. Furthermore, the group counts with private and semi-private investment through various affiliated companies.