An accessible podcast about Type Theory, Programming Languages Research and related topics.
Listen to episodes
60 recent
June 13, 20262 hr 4 min
#62 Dependent Haskell - Vladislav Zavialov
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
April 16, 20262 hr 19 min
#61 Zurihac Behind the Scenes - Farhad Mehta
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
March 25, 20261 hr 53 min
#60 Conversations on Life, AI, and the PL Job Market - Pedro and Dan
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
January 28, 20262 hr 46 min
#59 Category Theory and Inclusivity - Valeria de Paiva
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
December 16, 20252 hr 18 min
#58 Constructivism and Computational Content - Andrej Bauer
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
December 6, 202559 min
#57 Compilers for Privacy-Preserving Computation, Category Theory, and Keeping a Good Rythm in your PhD - Raghav Malik
Raghav Malik, has just defended his PhD on the topic of compilers for privacy-preserving computation, and that's a good chunk of our conversation.
He has also spent some years in grad school going down the rabbit hole to actually learn Category Theory in depth and from first principles, so I was deieing to ask him if category theory is really all that to learn the foundations of PL. In other words, does learning category theory really make you a better PL researcher?
Then, of course, I wouldn’t finish this episode without asking him how he coped with Mental Health during his PhD Journey.
Links
Raghav's Website
TTFA Patreon
TTFA Merch Store
TTFA Ko-Fi
November 17, 20251 hr 36 min
#56 Property Based Testing and PL Grad School Applications - Francille Zhuang
Francille Zhuang is an undergrad at Purdue University and has been doing research with Benjamin Delaware and Patrick Lafontaine. In this episode we talk about her early research experiences on Property Based Testing, and we go through all the necessary information for applying for graduate school in Programming Languages in the US.
Links
Francille's LinkedIn
TTFA Mentorship Program
TTFA Merch Store
TTFA Patreon
TTFA Ko-Fi
October 27, 20252 hr 38 min
#55 The Death of OO, The Beauty of Scheme, BobKonf, and FunArch - Mike Sperber
Mike Sperber is the CEO of Active Group, a company designed for Counseling, Development and Training in functional programming. He is a co-organizer of Bob Konf and FunArch, the Co-founder of the leading german blog on functional programming. Member of the Editorial Board of the JFP. Part of the R6RS, the 6th revised report on the Algorithmic Language Scheme.
In our conversation we talk about C, Lisp, Emacs Lisp, Scheme and his involvement with the R6RS. His views on mathematics and formal methods as languages, his views on the use of Functional Programming in the Industry, his thoughts of how Object Oriented Programming is dead. Macros, hygienic macros and much more!
We also talk about BobKonf and FunArch as amazing confereces on Functional Programming and their design and archtechture. BobKonf currently has a call for talks open and goes until november 17th.
Consider supporting the show!
TTFA Patreon
One time donations
Merch Store
Links
Mike's Website
Bob Konf
FunArch
Functional Programming Blog
TTFA Graduate Mentorship
September 29, 20251 hr 50 min
#54 The Goal of Science is to Communicate Ideas! - Philip Wadler
Philip Wadler is a well known, celebrated and recognized researcher in the field especially for his unique ability to explain complex ideas in a simple and elegant way. He got his Bachelor in 1977 at Stanford, his Masters in 1979 and his PhD in 1984 both at CMU. In 2023, he was awarded the distinguished honor of being elected a Fellow of the Royal Society, joining the ranks of scientific greats such as Isaac Newton and Charles Darwin.
Wadler describes himself as someone who likes to bring theory into practice, and practice into theory. In this episode, we talk about his prolific research, the story behind Monads and Type Classes, Category Theory and Homotopy Type Theory.
Throughout our conversation, in response to my eagerness to understand the philosophy and method behind his remarkable papers, he repeatedly emphasizes that the whole point of science is clearly communicating ideas so that others can build upon them.
Links
Wadler's Website
Ullman's Advising Students For Success
Grad School Mentorship
Consider contributing to this show through our ko-fi!
August 27, 20252 hr 25 min
#53 RustBelt, Iris, and the Art of Writing - Derek Dreyer
Derek Dreyer is a professor at the Max Planck Institute, in 2024 he was awarded the ACM Fellowship, in 2017 he got the ACM Sigplan Robin Milner Young Researcher Award. And has participated or lead greatly influential work, such as the RustBelt Project and Iris.
In this episode Derek shares his experience going to Grad School at CMU, how even a great research as himself has fallen pray to the impostor syndrome and how to cope with it. Throughout the conversation he makes beautiful parallels between music and academic papers, and how the work of a researcher is similar to that of an artist an many aspects. He also gives us a few tips about how to become a better academic writer. And of course, we also talked about Rust and the history about formally verifying its type system.
Don't forget to check our merch store!
Links
Derek's Website
POPL '25 PLMW Talk - How to Write Papers so that People Can Read Them
Is this your show?
Claim this listing to keep it up to date, reach guests who want to pitch you, and manage bookings with Guestify.
