Type Theory Forall

Type Theory much beyond inference rules

Check out our brand new store!

Grab Type Theory goodies and support the podcast!

Last Episodes

#52 Why is Haskell so special

Lennart Augustsson

Lennart Augustsson has spent the last four decades quietly — and sometimes mischievously — shaping the way we think about code. He co-authored *Lazy ML* in the early 80s, wrote *A Compiler for LML* b

Jul 10th 2025 91 min

#51 s/Coq/Rocq

Nicolas Tabareau

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. The original idea of this interview is to talk about the r

Jun 4th 2025 102 min

join our discord

All Episodes

#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

join our discord