Type Theory Forall

Check out our merch store!

Grab Type Theory goodies and support the podcast!

Last Episodes

#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 lead

Oct 27th 2025 158 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

Sep 29th 2025 110 min

RSS-Feed

All Episodes

#53 RustBelt, Iris, and the Art of Writing

Derek Dreyer

Aug 27th 2025 | 145 min

#52 Why is Haskell so special

Lennart Augustsson

Jul 10th 2025 | 91 min

#51 s/Coq/Rocq

Nicolas Tabareau

Jun 4th 2025 | 102 min

#50 The Expression Problem, Functional Pearls, Program Calculation

Wouter Swierstra

May 14th 2025 | 127 min

#49 Self-Education in PL

Ryan Brewer

Mar 14th 2025 | 144 min

#48 Bell Labs

David MacQueen

Jan 21st 2025 | 130 min

#47 The History of LCF, ML and HOPE

David MacQueen

Jan 7th 2025 | 125 min

#46 Realizability, BHK, CPS Translation, Dialectica

Pierre-Marie Pédrot

Nov 29th 2024 | 64 min

#45 What is Type Theory and What Properties we Should Care About

Pierre-Marie Pédrot

Nov 24th 2024 | 82 min

#44 Theorem Prover Foundations, Lean4Lean, Metamath

Mario Carneiro

Nov 6th 2024 | 134 min

#43 PL in the Industry and Summer Schools

Patrick and Eric

Sep 13th 2024 | 62 min

#42 Distributed Systems, Microservices, and Choreographies

Fabrizio Montesi

Aug 29th 2024 | 113 min

#41 The Value of PL (and) Education

Satnam Singh

Aug 15th 2024 | 101 min

#40 Secure Voting

Joe Kiniry

Jul 15th 2024 | 69 min

#39 Equality, Quotation, Bidirectional Type Checking

David Christiansen

Jun 13th 2024 | 110 min

#38 Haskell, Lean, Idris, and the Art of Writing

David Christiansen

May 16th 2024 | 116 min

#37 Compilers, Staging, Futamura Projections

Guannan Wei

Mar 11th 2024 | 113 min

#36 Behind the Person Behind this Podcast

Pedro Abreu

Dec 26th 2023 | 110 min

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

Eduardo Rafael

Dec 4th 2023 | 81 min

#34 Foundations of Theorem Provers and Cedille2

Andrew Marmaduke

Oct 16th 2023 | 88 min

#33 Z3 and Lean, the Spiritual Journey

Leo de Moura

Sep 9th 2023 | 125 min

#32 TyDe Systems

Jan de Muijnck-Hughes

Jul 22nd 2023 | 101 min

#31 Discussing Problems in PL and Academia

Jan de Muijnck-Hughes

Jul 13th 2023 | 130 min

#30 Actors, GADTs and Burnout

Dan and Pedro

May 30th 2023 | 105 min

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

Jimmy Koppel

Apr 9th 2023 | 84 min

#28 Formally Verifying Smart Contracts

Pruvendo

Feb 15th 2023 | 71 min

#27 Formalizing an OS: The seL4

Gerwin Klein

Feb 4th 2023 | 119 min

#26 Mechanizing Modern Mathematics

Kevin Buzzard

Jan 16th 2023 | 136 min

#25 Formally Verifying the Tezos Codebase

Formal Land

Nov 21st 2022 | 62 min

#24 The History of Isabelle

Lawrence Paulson

Oct 6th 2022 | 98 min

#23 What is the SIGPLAN?

Jens Palsberg and Jonathan Aldrich

Sep 24th 2022 | 72 min

#22 Impredicativity, LEM, Realizability and more

Cody Roux

Aug 12th 2022 | 139 min

#21 Denotational Design

Conal Elliott

Aug 4th 2022 | 187 min

#20 Huaweii, String Diagrams, Game Semantics

Dan R. Ghica

Jun 28th 2022 | 97 min

#19 Experience Report: Learning Coq

Patrick and Supun

Jun 4th 2022 | 112 min

#18 Gödel's Incompleteness Theorems

Cody Roux

May 19th 2022 | 170 min

#17 The Lost Elegance of Computation

Conal Elliott

May 9th 2022 | 213 min

#16 Agda, K Axiom, HoTT, Rewrite Theory

Jesper Cockx

Apr 2nd 2022 | 96 min

#15 Coq Projects, Agda, Idris, Kind

Nitin and Eric

Mar 27th 2022 | 78 min

#14 POPL, Parametricity, Scala, DOT

Nitin and Eric

Feb 12th 2022 | 57 min

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

John Wiegley

Dec 23rd 2021 | 100 min

#12 Tenure, Sexism and ADHD

Talia Ringer

Nov 10th 2021 | 66 min

#11 FP, Monads, GHC, and beyond

Alejandro Serrano

Oct 4th 2021 | 67 min

#10 Classical Logic vs Intuitionistic Logic

Thorsten Altenkirch and Anupam Das

Jul 15th 2021 | 77 min

#9 Logic and Proof Theory

Anupam Das

May 28th 2021 | 57 min

#8 Cedille

Chris Jenkins

May 11th 2021 | 66 min

#7 Hacking Isabelle's Internals

Dan Matichuk

Apr 16th 2021 | 81 min

#6 All The Dumb Questions on Gradual Types

Zeina Migeed

Mar 29th 2021 | 39 min

#5 The History of Coq'Art

Yves Bertot

Feb 27th 2021 | 72 min

#4 Theorem Provers, Functional Programming and Companies

Eric Bond

Feb 15th 2021 | 74 min

#3 ML for PL and Mental Health

Dan Zheng

Feb 1st 2021 | 68 min

#2 Grad School Life

Rajan Walia and John Sarracino

Jan 10th 2021 | 77 min

#1 What is PL research?

Prof. Ben Delaware

Dec 23rd 2020 | 58 min

#0 Cool Internships in PL

Pedro Abreu

Dec 14th 2020 | 32 min