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.

People involved

Avatar

Alfonso Alfaro

University of Barcelona

Researcher

Avatar

Ana Borges

University of Barcelona

Researcher

Avatar

Esperanza Buitrago

University of Barcelona

Researcher

Avatar

Joost J. Joosten

University of Barcelona

Group Coordinator

Avatar

Albert Atserias

Polytechnic University of Catalonia

Full Professor

Avatar

Aleix Solé

University of Barcelona

Researcher

Avatar

Eduardo Hermo

University of Barcelona

Researcher

Avatar

Eric Sancho

University of Barcelona

Researcher

Avatar

Jan Mas

University of Barcelona

Researcher

Avatar

Juan Conejero

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