Type Theory Forall

#59 Category Theory and Inclusivity - Valeria de Paiva

28 Jan 2026

Contributed by Lukas

In this episode of the Type Theory Forall podcast, we are joined by Valeria de Paiva, a Brazilian mathematician and logician whose work has ha...

#58 Constructivism and Computational Content - Andrej Bauer

16 Dec 2025

Contributed by Lukas

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 co...

#57 Compilers for Privacy-Preserving Computation, Category Theory, and Keeping a Good Rythm in your PhD - Rhagav Malik

06 Dec 2025

Contributed by Lukas

Rhagav Malik, has just defended his PhD on the topic of compilers for privacy-preserving computation, and that's a good chunk of our conversat...

#56 Property Based Testing and PL Grad School Applications - Francille Zhuang

17 Nov 2025

Contributed by Lukas

Francille Zhuang is an undergrad at Purdue University and has been doing research with Benjamin Delaware and Patrick Lafontaine. In this episo...

#55 The Death of OO, The Beauty of Scheme, BobKonf, and FunArch - Mike Sperber

27 Oct 2025

Contributed by Lukas

Mike Sperber is the CEO of Active Group, a company designed for Counseling, Development and Training in functional programming. He is a co-org...

#54 The Goal of Science is to Communicate Ideas! - Philip Wadler

29 Sep 2025

Contributed by Lukas

Philip Wadler is a well known, celebrated and recognized researcher in the field especially for his unique ability to explain complex ideas in...

#53 RustBelt, Iris, and the Art of Writing - Derek Dreyer

27 Aug 2025

Contributed by Lukas

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 Milne...

#52 Why is Haskell so special - Lennart Augustsson

10 Jul 2025

Contributed by Lukas

Lennart Augustsson has spent the last four decades quietly — and sometimes mischievously — shaping the way we think about code. He co-auth...

#51 s/Coq/Rocq - Nicolas Tabareau

04 Jun 2025

Contributed by Lukas

In this episode we talk with Nicolas Tabareau, the Head of Gallinette, one of the main teams which develop the Rocq theorem Prover at Inria. T...

#50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra

14 May 2025

Contributed by Lukas

Wouter Swierstra is a Math Bachelor’s from the University of Utrecht, has done his PhD with Thorsten Altenkirch at the University of Notting...

#49 Self-Education in PL - Ryan Brewer

14 Mar 2025

Contributed by Lukas

Ryan Brewer is a college dropout who has an incredible blog about PL, Category Theory and Logic. He better define his goal as making Formal Th...

#48 Bell Labs - David MacQueen

21 Jan 2025

Contributed by Lukas

In this episode we continue with our conversation with David MacQueen, he is an Emeritus Professor from the University of Chicago, and has wor...

#47 The History of LCF, ML and HOPE - David MacQueen

07 Jan 2025

Contributed by Lukas

David MacQueen has worked at Bell Labs for around 20 years during it’s Golden Age. Professor at Chicago University for 23 years. He is one o...

#46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie Pédrot

29 Nov 2024

Contributed by Lukas

In this episode Pierre-Marie Pédrot, one of the main Coq/Rocq developers joins us to talk about Krivine, Kleene and Gödel Realizability Mode...

#45 What is Type Theory and What Properties we Should Care About - Pierre-Marie Pédrot

24 Nov 2024

Contributed by Lukas

In this episode Pierre-Marie Pédrot who is one of the main Coq/Rocq developers joins us to talk about what is Type Theory, what is Martin-Lö...

#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro

06 Nov 2024

Contributed by Lukas

Mario Carneiro is the creator of Mathlib, Lean4Lean and Metamath0. He is currently doing his Postdoc at Chalmers University working on CakeML....

#43 PL in the Industry and Summer Schools - Patrick and Eric

13 Sep 2024

Contributed by Lukas

In this episode Eric Bond and Patrick Lafontaine joins us to talk about the life in industry vs the life in academia. Eric is a PhD student at...

#42 Distributed Systems, Microservices, and Choreographies - Fabrizio Montesi

29 Aug 2024

Contributed by Lukas

In this episode we talk with Fabrizio Montesi, a Full Professor at the University of South Denmark. He is one of the creators of the Jolie Pro...

#41 The Value of PL (and) Education - Satnam Singh

15 Aug 2024

Contributed by Lukas

Satnam Singh has got incredible experience in both academia and industry. He has worked in Google, Facebook, Microsoft, Microsoft Research, Xi...

#40 Secure Voting - Joe Kiniry

15 Jul 2024

Contributed by Lukas

In this episode we go into a deep dive into the formal methods side of Voting systems, and for this nobody better than our guest: Joe Kiniry, ...

#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen

13 Jun 2024

Contributed by Lukas

In this episode we continue our conversation with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer. ...

#38 Haskell, Lean, Idris, and the Art of Writing - David Christiansen

16 May 2024

Contributed by Lukas

In this episode we talk with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer. He has also worked as...

#37 Compilers, Staging, Futamura Projections - Guannan Wei

11 Mar 2024

Contributed by Lukas

In this episode we talk with Guannan Wei, from Purdue University. Guannan finished his PhD last year under Tiark Rompf, and is currently doing...

#36 Behind the Person Behind this Podcast - Pedro Abreu

26 Dec 2023

Contributed by Lukas

In this episode we celebrate 3 years of existence of this podcast by reflecting on the journey so far, what is my philosophy, how do I approac...

#35 Teika, Self-Education and F***ing Floating Points - Eduardo Rafael

04 Dec 2023

Contributed by Lukas

In this episode we talk with Eduardo Rafael. He is self-thaught programming languages enthusiast, youtuber, twitch streamer, multi-skilled pro...

#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke

16 Oct 2023

Contributed by Lukas

Andrew Marmaduke is a PhD Candidate from the University of Iowa, he works under Aaron Stump and has been working on revamping the theorem prov...

#33 Z3 and Lean, the Spiritual Journey - Leo de Moura

09 Sep 2023

Contributed by Lukas

Not satisfied with implementing one of the most popular automated theorem provers, Z3, Leo de Moura also tackles another extremely hard proble...

#32 TyDe Systems - Jan de Muijnck-Hughes

22 Jul 2023

Contributed by Lukas

In this episode we continue our conversation with Jan de Muijnck-Hughes a Research Associate at Glasgow University. He works using all sorts o...

#31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes

13 Jul 2023

Contributed by Lukas

In this episode we have a deep conversation with Jan de Muijnck-Hughes, talks about all the cool research he has done with idris, hardware and...

#30 Actors, GADTs and Burnout - Dan and Pedro

30 May 2023

Contributed by Lukas

In this episode we have over Dan Plyukhin, a PhD Candidate from the University of Illinois Urbana-Champaign. We talk about Dan’s research is...

#29 Can PL theory make you a better software engineer? - Jimmy Koppel

09 Apr 2023

Contributed by Lukas

Jimmy Koppel, got his PhD at MIT and found the Mirdin Company, where he teaches engineers to write better code! In this interview we talk abou...

#28 Formally Verifying Smart Contracts - Pruvendo

15 Feb 2023

Contributed by Lukas

In this episode we host another company that does formal method in the context of the Everscale Blockchain, and Solidity smart contracts. How ...

#27 Formalizing an OS: The seL4 - Gerwin Klein

04 Feb 2023

Contributed by Lukas

In this episode talk with Gerwin Klein about the formal verification of the microkernel seL4 which was done using Isabelle at NICTA / Data61 i...

#26 Mechanizing Modern Mathematics - Kevin Buzzard

16 Jan 2023

Contributed by Lukas

Kevin Buzzard has been very passionate spreading the word among mathematicians to use theorem provers mechanize theorems of modern mathematics...

#25 Formally Verifying the Tezos Codebase - Formal Land

21 Nov 2022

Contributed by Lukas

In this episode we partner with Formal Land, a company that works in formally verifying the Tezos codebase! I have worked with them in the pas...

#24 The History of Isabelle - Lawrence Paulson

06 Oct 2022

Contributed by Lukas

In this episode we interview Lawrence Paulson, one of the creating fathers of Isabelle. We talk about the development process, how it drew ins...

#23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich

24 Sep 2022

Contributed by Lukas

In this episode we talk about Sigplan, the organization behind the most important conferences and proceedings in our field. What is the SIGPLA...

#22 Impredicativity, LEM, Realizability and more - Cody Roux

12 Aug 2022

Contributed by Lukas

In this episode Cody Roux teaches some interesting concepts that people care about in Mathematics and Logic as a way to try to understand what...

#21 Denotational Design - Conal Elliott

04 Aug 2022

Contributed by Lukas

In this episode Conal Elliott gives a more concrete presentation on what is Denotational Design is and how to use it in practice. It is a cont...

#20 Huaweii, String Diagrams, Game Semantics - Dan R. Ghica

28 Jun 2022

Contributed by Lukas

In this episode, me and Eric Bond have a great conversation with Dan R. Ghica, a professor at Birmingham University and Director of the Progra...

#19 Experience Report: Learning Coq - Patrick and Supun

04 Jun 2022

Contributed by Lukas

In today’s episode I invite two friends of mine Patrick Lafontaine and Supun Abeysinghe. We will talk about their experience learning Coq an...

#18 Gödel's Incompleteness Theorems - Cody Roux

19 May 2022

Contributed by Lukas

In this episode Cody Roux talks about the Gödel's Incompleteness Theorems. We go through it’s underlying historical context, Hilbert’s Pr...

#17 The Lost Elegance of Computation - Conal Elliott

09 May 2022

Contributed by Lukas

In this episode I had the pleasure to have an in-depth conversation with Conal Elliott about his life, his work, his philosophy and his many o...

#16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx

02 Apr 2022

Contributed by Lukas

In this episode we interview Jesper Cockx, one of the core developers on Agda. We talk about the philosophy behind Agda, his work on pattern m...

#15 Coq Projects, Agda, Idris, Kind - Nitin and Eric

27 Mar 2022

Contributed by Lukas

In this episode me, Eric and Nitin continues our conversation started in the last episode. This time we move our attention to the cool project...

#14 POPL, Parametricity, Scala, DOT - Nitin and Eric

12 Feb 2022

Contributed by Lukas

In this episode I gather with two good friends Eric and Nitin to randomly talk random subjects that pops up. Among them we talked about POPL, ...

#13 C/C++, Emacs, Haskell, and Coq. The Journey - John Wiegley

23 Dec 2021

Contributed by Lukas

This episode is about the journey of a programmer that converted himself into a Haskell developer after working with C/C++ for more than 10yea...

#12 Tenure, Sexism and ADHD - Talia Ringer

10 Nov 2021

Contributed by Lukas

Talia Ringer is an Assistant Professor at University of Illinois Urbana-Champaign. She did her PhD at University of Washington with her thesi...

#11 FP, Monads, GHC, and beyond - Alejandro Serrano

04 Oct 2021

Contributed by Lukas

In this episode we have talk with Alejandro Serrano Mena, he works on 47 degrees and is a published author of two books about Haskell: The Boo...

#10 Classical Logic vs Intuitionistic Logic - Thorsten Altenkirch and Anupam Das

15 Jul 2021

Contributed by Lukas

In this episode we host a discussion between Anupam Das and Thorsten Altenkirch on the role of constructivism in mathematics, logic and comput...

#9 Logic and Proof Theory - Anupam Das

28 May 2021

Contributed by Lukas

#8 Cedille - Chris Jenkins

11 May 2021

Contributed by Lukas

In this episode I have a nice conversation with Chris Jenkins to talk about the Cedille theorem prover, based on a very concise type theory ca...

#7 Hacking Isabelle's Internals - Dan Matichuk

16 Apr 2021

Contributed by Lukas

In this episode we dive into Isabelle, the interactive theorem prover based on Higher Order Logic directly from someone who spent quite some t...

#6 All The Dumb Questions on Gradual Types - Zeina Migeed

29 Mar 2021

Contributed by Lukas

In this episode we interview Zeina Migeed, a PhD Student at University of California Los Angeles, advised by Prof. Jens Palsberg She Researche...

#5 The History of Coq'Art - Yves Bertot

27 Feb 2021

Contributed by Lukas

In this episode we interview Yves Bertot and we talk about the history behind his contribution with Pierre Castéran on writing Coq’Art. Wha...

#4 Theorem Provers, Functional Programming and Companies - Eric Bond

15 Feb 2021

Contributed by Lukas

In this episode we host Eric Bond to go through some real cool projects happening in the PL World and some of the companies behind them. We di...

#3 ML for PL and Mental Health - Dan Zheng

01 Feb 2021

Contributed by Lukas

In this episode we host Dan Zheng, an alumni of Purdue University that now works at Google at real cool projects that relates ML and PL. We ch...

#2 Grad School Life - Rajan Walia and John Sarracino

10 Jan 2021

Contributed by Lukas

In this episode we host Rajan Walia and John Sarracino. Rajan is a last year PhD Student from Indiana University, working under Sam Tobin-Hoch...

#1 What is PL research? - Prof. Ben Delaware

23 Dec 2020

Contributed by Lukas

In this episode we host Prof. Benjamin Delaware from Purdue University to discuss and try to answer some basic questions related to PL researc...

#0 Cool Internships in PL - Pedro Abreu

14 Dec 2020

Contributed by Lukas

Who is Pedro Abreu? What is the goal of this Podcast? What are My Research Interests? In this episode I share about my internship experiences ...