What we do

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.

What we do

People involved

Avatar

Joost J. Joosten

Universitat de Barcelona

Group Coordinator

Avatar

Sofía Santiago

Universitat de Barcelona

Researcher

Avatar

Ana Borges

Universitat de Barcelona

Researcher

Avatar

Albert Atserias

Universitat Politècnica de Catalunya

University Professor

Avatar

David Fernández-Duque

Universitat de Barcelona

University Professor

Avatar

Eduardo Hermo

University of Barcelona

Researcher

Avatar

Jan Mas

University of Barcelona

Researcher

Avatar

Maria Lluisa Bonet

Polytechnic University of Catalonia

University Professor

Avatar

Mireia González

University of Barcelona

Researcher

Avatar

Moritz Müller

Polytechnic University of Catalonia

Researcher

Avatar

Quim Casals

University of Barcelona

Researcher