Type Theory Forall
By Pedro Abreu
Listen to a podcast, please open Podcast Republic app. Available on Google Play Store and Apple App Store.
Image by Pedro Abreu
Category: Technology
Open in Apple Podcasts
Open RSS feed
Open Website
Rate for this podcast
Subscribers: 19
Reviews: 0
Episodes: 62
Description
An accessible podcast about Type Theory, Programming Languages Research and related
topics.
| Episode | Date |
|---|---|
|
#61 Zurihac Behind the Scenes - Farhad Mehta
|
Apr 16, 2026 |
|
#60 Conversations on Life, AI, and the PL Job Market - Pedro and Dan
|
Mar 25, 2026 |
|
#59 Category Theory and Inclusivity - Valeria de Paiva
|
Jan 28, 2026 |
|
#58 Constructivism and Computational Content - Andrej Bauer
|
Dec 16, 2025 |
|
#57 Compilers for Privacy-Preserving Computation, Category Theory, and Keeping a Good Rythm in your PhD - Raghav Malik
|
Dec 06, 2025 |
|
#56 Property Based Testing and PL Grad School Applications - Francille Zhuang
|
Nov 17, 2025 |
|
#55 The Death of OO, The Beauty of Scheme, BobKonf, and FunArch - Mike Sperber
|
Oct 27, 2025 |
|
#54 The Goal of Science is to Communicate Ideas! - Philip Wadler
|
Sep 29, 2025 |
|
#53 RustBelt, Iris, and the Art of Writing - Derek Dreyer
|
Aug 27, 2025 |
|
#52 Why is Haskell so special - Lennart Augustsson
|
Jul 10, 2025 |
|
#51 s/Coq/Rocq - Nicolas Tabareau
|
Jun 04, 2025 |
|
#50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra
|
May 14, 2025 |
|
#49 Self-Education in PL - Ryan Brewer
|
Mar 14, 2025 |
|
#48 Bell Labs - David MacQueen
|
Jan 21, 2025 |
|
#47 The History of LCF, ML and HOPE - David MacQueen
|
Jan 07, 2025 |
|
#46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie Pédrot
|
Nov 29, 2024 |
|
#45 What is Type Theory and What Properties we Should Care About - Pierre-Marie Pédrot
|
Nov 24, 2024 |
|
#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro
|
Nov 06, 2024 |
|
#43 PL in the Industry and Summer Schools - Patrick and Eric
|
Sep 13, 2024 |
|
#42 Distributed Systems, Microservices, and Choreographies - Fabrizio Montesi
|
Aug 29, 2024 |
|
#41 The Value of PL (and) Education - Satnam Singh
|
Aug 15, 2024 |
|
#40 Secure Voting - Joe Kiniry
|
Jul 15, 2024 |
|
#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen
|
Jun 13, 2024 |
|
#38 Haskell, Lean, Idris, and the Art of Writing - David Christiansen
|
May 16, 2024 |
|
#37 Compilers, Staging, Futamura Projections - Guannan Wei
|
Mar 11, 2024 |
|
#36 Behind the Person Behind this Podcast - Pedro Abreu
|
Dec 26, 2023 |
|
#35 Teika, Self-Education and F***ing Floating Points - Eduardo Rafael
|
Dec 04, 2023 |
|
#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke
|
Oct 16, 2023 |
|
#33 Z3 and Lean, the Spiritual Journey - Leo de Moura
|
Sep 09, 2023 |
|
#32 TyDe Systems - Jan de Muijnck-Hughes
|
Jul 22, 2023 |
|
#31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes
|
Jul 13, 2023 |
|
#30 Actors, GADTs and Burnout - Dan and Pedro
|
May 30, 2023 |
|
#29 Can PL theory make you a better software engineer? - Jimmy Koppel
|
Apr 09, 2023 |
|
#28 Formally Verifying Smart Contracts - Pruvendo
|
Feb 15, 2023 |
|
#27 Formalizing an OS: The seL4 - Gerwin Klein
|
Feb 04, 2023 |
|
#26 Mechanizing Modern Mathematics - Kevin Buzzard
|
Jan 16, 2023 |
|
#25 Formally Verifying the Tezos Codebase - Formal Land
|
Nov 21, 2022 |
|
#24 The History of Isabelle - Lawrence Paulson
|
Oct 06, 2022 |
|
#23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich
|
Sep 24, 2022 |
|
#22 Impredicativity, LEM, Realizability and more - Cody Roux
|
Aug 12, 2022 |
|
#21 Denotational Design - Conal Elliott
|
Aug 04, 2022 |
|
#20 Huaweii, String Diagrams, Game Semantics - Dan R. Ghica
|
Jun 28, 2022 |
|
#19 Experience Report: Learning Coq - Patrick and Supun
|
Jun 04, 2022 |
|
#18 Gödel's Incompleteness Theorems - Cody Roux
|
May 19, 2022 |
|
#17 The Lost Elegance of Computation - Conal Elliott
|
May 09, 2022 |
|
#16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx
|
Apr 02, 2022 |
|
#15 Coq Projects, Agda, Idris, Kind - Nitin and Eric
|
Mar 27, 2022 |
|
#14 POPL, Parametricity, Scala, DOT - Nitin and Eric
|
Feb 12, 2022 |
|
#13 C/C++, Emacs, Haskell, and Coq. The Journey - John Wiegley
|
Dec 23, 2021 |
|
#12 Tenure, Sexism and ADHD - Talia Ringer
|
Nov 10, 2021 |
|
#11 FP, Monads, GHC, and beyond - Alejandro Serrano
|
Oct 04, 2021 |
|
#10 Classical Logic vs Intuitionistic Logic - Thorsten Altenkirch and Anupam Das
|
Jul 15, 2021 |
|
#9 Logic and Proof Theory - Anupam Das
|
May 28, 2021 |
|
#8 Cedille - Chris Jenkins
|
May 11, 2021 |
|
#7 Hacking Isabelle's Internals - Dan Matichuk
|
Apr 16, 2021 |
|
#6 All The Dumb Questions on Gradual Types - Zeina Migeed
|
Mar 29, 2021 |
|
#5 The History of Coq'Art - Yves Bertot
|
Feb 27, 2021 |
|
#4 Theorem Provers, Functional Programming and Companies - Eric Bond
|
Feb 15, 2021 |
|
#3 ML for PL and Mental Health - Dan Zheng
|
Feb 01, 2021 |
|
#2 Grad School Life - Rajan Walia and John Sarracino
|
Jan 10, 2021 |
|
#1 What is PL research? - Prof. Ben Delaware
|
Dec 23, 2020 |
|
#0 Cool Internships in PL - Pedro Abreu
|
Dec 14, 2020 |