Type Theory Forall

Vlad works at Serokell to develop the Glasgow Haskell Compiler, he is a former member of the Haskell Steering Committee and the current implementer of Dependent Haskell.

In this conversation we talk about the development process of the GHC, he explains with detail how’s the decision process of the community to modify the language through the Haskell Steering Committee. And we get pretty technical discussing the GHC internals, he basically gives us a class of how things looks like and how can a newcomer start hacking the GHC today.

And of course, we go into details of the theory and implementation of Dependent Haskell!

Links

Serokell
Serokell on X
Vlad on X
Dependent Haskell Roadmap

If you enjoy the show please consider supporting us: https://www.typetheoryforall.com/patreon

In this episode we talk with Farhad Mehta, one of the main organizers of Zurihac, the biggest Haskell event in the planet.

Zurihac happens once a year at Zurich. This year’s Zurihac will be on june 6, 7 and 8.

Links

Zurihac Website

Types Discussion on the use of AI

Agda Discussion on the use of AI

In this episode me and Dan Plyukhin get together to have a heartfelt conversation. We start by talking about our experiences with meditation, and how it has helped us to have a more balanced work-life experience. Then the conversation shifts to comment about the current situation of the job market. Both in academia and in industry. We talk about strategies to reach out to professors and our view on the use of AI in general, and of course we talk about our current research interests.

Links

Consider being a Patreon

Check out our merch!

Any donations are highly appreciated! Link to Ko-Fi

Dan's Website

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.

🔗 Links

👩‍🏫 Valeria de Paiva

Website

Twitter / X

Women in Logic

Topos Institute

📚 Type Theory Forall

TTFA Store

Patreon

Andrej Bauer has done his PhD at CMU under Dana Scott, and he stands right on the edge between mathematics and computer science. During our conversation it just feels that he can just go on in depth about any topic remotely related to Type Theory and Programming Languages.

Andrej is the person who organized for the The Proof Assistants stack exchange. He has an incredible blog that’s always a great resource to learn Type Theory and Programming Languages Theory. He also has an incredible series of summer school lectures on effect handlers.

But more specifically today we talk about Constructivism, Dialectica, Effect Handlers and AI. I’m sure you guys are gonna love it!

Links

Andrej's Website

Andrej's Blog