Type Theory Forall

Type Theory much beyond inference rules

Last Episodes

#65 TLA+, Quint and Formal Verification in the Age of AI

Gabriela Moreira

How can we be sure that our code is doing what is supposed to be doing? And this is the role of formal verification at large: A Discipline to trust that the code is doing what it is supposed to do.

Oct 19th 2026 2h03min

#64 PL Education in the Age of AI

Shriram Krishnamurthi

Shriram has devoted his Career to advance the teaching of programming of programming languages. he is a professor at Brown, The author / co-author of different books about this, and a major contributo

Sep 5th 2026 2h44min

join our discord

All Episodes

#63 Hack: Typing PHP at Facebook Scale

Julien Verlaguet

Aug 7th 2026 | 1h46min

#62 Dependent Haskell

Vladislav Zavialov

Jun 13th 2026 | 2h05min

#61 Zurihac Behind the Scenes

Farhad Mehta

Apr 16th 2026 | 2h19min

#60 Conversations on Life, AI, and the PL Job Market

Pedro and Dan

Mar 25th 2026 | 1h53min

#59 Category Theory and Inclusivity

Valeria de Paiva

Jan 28th 2026 | 2h47min

#58 Constructivism and Computational Content

Andrej Bauer

Dec 16th 2025 | 2h19min

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

Raghav Malik

Dec 6th 2025 | 59 min

#56 Property Based Testing and PL Grad School Applications

Francille Zhuang

Nov 17th 2025 | 1h36min

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

Mike Sperber

Oct 27th 2025 | 2h38min

#54 The Goal of Science is to Communicate Ideas!

Philip Wadler

Sep 29th 2025 | 1h50min

#53 RustBelt, Iris, and the Art of Writing

Derek Dreyer

Aug 27th 2025 | 2h25min

#52 Why is Haskell so special

Lennart Augustsson

Jul 10th 2025 | 1h31min

#51 s/Coq/Rocq

Nicolas Tabareau

Jun 4th 2025 | 1h42min

#50 The Expression Problem, Functional Pearls, Program Calculation

Wouter Swierstra

May 14th 2025 | 2h07min

#49 Self-Education in PL

Ryan Brewer

Mar 14th 2025 | 2h24min

#48 Bell Labs

David MacQueen

Jan 21st 2025 | 2h10min

#47 The History of LCF, ML and HOPE

David MacQueen

Jan 7th 2025 | 2h05min

#46 Realizability, BHK, CPS Translation, Dialectica

Pierre-Marie Pédrot

Nov 29th 2024 | 1h04min

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

Pierre-Marie Pédrot

Nov 24th 2024 | 1h22min

#44 Theorem Prover Foundations, Lean4Lean, Metamath

Mario Carneiro

Nov 6th 2024 | 2h14min

#43 PL in the Industry and Summer Schools

Patrick and Eric

Sep 13th 2024 | 1h02min

#42 Distributed Systems, Microservices, and Choreographies

Fabrizio Montesi

Aug 29th 2024 | 1h53min

#41 The Value of PL (and) Education

Satnam Singh

Aug 15th 2024 | 1h41min

#40 Secure Voting

Joe Kiniry

Jul 15th 2024 | 1h09min

#39 Equality, Quotation, Bidirectional Type Checking

David Christiansen

Jun 13th 2024 | 1h50min

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

David Christiansen

May 16th 2024 | 1h56min

#37 Compilers, Staging, Futamura Projections

Guannan Wei

Mar 11th 2024 | 1h53min

#36 Behind the Person Behind this Podcast

Pedro Abreu

Dec 26th 2023 | 1h50min

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

Eduardo Rafael

Dec 4th 2023 | 1h21min

#34 Foundations of Theorem Provers and Cedille2

Andrew Marmaduke

Oct 16th 2023 | 1h28min

#33 Z3 and Lean, the Spiritual Journey

Leo de Moura

Sep 9th 2023 | 2h05min

#32 TyDe Systems

Jan de Muijnck-Hughes

Jul 22nd 2023 | 1h41min

#31 Discussing Problems in PL and Academia

Jan de Muijnck-Hughes

Jul 13th 2023 | 2h10min

#30 Actors, GADTs and Burnout

Dan and Pedro

May 30th 2023 | 1h45min

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

Jimmy Koppel

Apr 9th 2023 | 1h24min

#28 Formally Verifying Smart Contracts

Pruvendo

Feb 15th 2023 | 1h11min

#27 Formalizing an OS: The seL4

Gerwin Klein

Feb 4th 2023 | 1h59min

#26 Mechanizing Modern Mathematics

Kevin Buzzard

Jan 16th 2023 | 2h16min

#25 Formally Verifying the Tezos Codebase

Formal Land

Nov 21st 2022 | 1h02min

#24 The History of Isabelle

Lawrence Paulson

Oct 6th 2022 | 1h38min

#23 What is the SIGPLAN?

Jens Palsberg and Jonathan Aldrich

Sep 24th 2022 | 1h12min

#22 Impredicativity, LEM, Realizability and more

Cody Roux

Aug 12th 2022 | 2h19min

#21 Denotational Design

Conal Elliott

Aug 4th 2022 | 3h07min

#20 Huaweii, String Diagrams, Game Semantics

Dan R. Ghica

Jun 28th 2022 | 1h37min

#19 Experience Report: Learning Coq

Patrick and Supun

Jun 4th 2022 | 1h52min

Show more episodes

join our discord