Type Theory Forall

Type Theory much beyond inference rules

Last Episodes

#44 Theorem Prover Foundations, Lean4Lean, Metamath

Mario Carneiro

Mario Carneiro is the creator of Mathlib, Lean4Lean and Metamath0. He is currently doing his Postdoc at Chalmers University working on CakeML. In this episode we talk about foundations of theorem prov

Nov 6th 2024 134 min

#43 PL in the Industry and Summer Schools

Patrick and Eric

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 Michigan University under Max New, he works with some pre

Sep 13th 2024 62 min

join our discord

All Episodes

#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