Type Theory Forall

In this episode of the Type Theory Forall podcast, we are joined by Valeria de Paiva, a Brazilian mathematician and logician whose work has had a lasting influence on category theory, type theory, and the foundations of logic. She is also a co-founder of the Topos Institute, where she continues to explore deep connections between mathematics, logic, computation, and the sciences.

Valeria completed her PhD at Cambridge in the mid-1980s. Even today, pursuing an academic career abroad from Brazil is challenging; doing so at that time — and as a woman — required exceptional determination and resilience. Her trajectory alone already makes her an inspiring figure in the field.

This episode is one of the most technically focused conversations on category theory we have ever had on TTFA. Coming from a strong mathematics background, Valeria has worked extensively on categorical semantics, logical interpretations, and the interface between logic, computation, and language. As a result, the discussion goes deep into categorical ideas and their role in type theory.

Valeria is also the founder of the Women in Logic initiative, which enabled a serious and thoughtful discussion about gender inequality in logic, type theory, and computer science. The conversation is grounded not only in abstract principles, but in decades of concrete work building communities, workshops, and long-lasting support structures for women in the field.

Overall, this episode brings together technical depth, personal history, and a broader reflection on what it means to build a healthier and more inclusive research culture in logic and programming languages.