Type Theory Forall

Pedro Abreu
  • 4.8 (13)
  • TECHNOLOGY
  • UPDATED MONTHLY

An accessible podcast about Type Theory, Programming Languages Research and related topics.

  1. 12/16/2025

    #58 Constructivism and Computational Content - Andrej Bauer

    Andrej Bauer has done his PhD at CMU under Dana Scott, and he stands right on the edge between mathematics and computer science. During our conversation it just feels that he can just go on in depth about any topic remotely related to Type Theory and Programming Languages. Andrej is the person who organized for the The Proof Assistants stack exchange. He has an incredible blog that’s always a great resource to learn Type Theory and Programming Languages Theory. He also has an incredible series of summer school lectures on effect handlers. But more specifically today we talk about Constructivism, Dialectica, Effect Handlers and AI. I’m sure you guys are gonna love it! Links Andrej's Website Andrej's Blog

    2h 19m

  2. 12/06/2025

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

    Raghav Malik, has just defended his PhD on the topic of compilers for privacy-preserving computation, and that's a good chunk of our conversation. He has also spent some years in grad school going down the rabbit hole to actually learn Category Theory in depth and from first principles, so I was deieing to ask him if category theory is really all that to learn the foundations of PL. In other words, does learning category theory really make you a better PL researcher? Then, of course, I wouldn’t finish this episode without asking him how he coped with Mental Health during his PhD Journey. Links Raghav's Website TTFA Patreon TTFA Merch Store TTFA Ko-Fi

    59 min

  3. 11/17/2025

    #56 Property Based Testing and PL Grad School Applications - Francille Zhuang

    Francille Zhuang is an undergrad at Purdue University and has been doing research with Benjamin Delaware and Patrick Lafontaine. In this episode we talk about her early research experiences on Property Based Testing, and we go through all the necessary information for applying for graduate school in Programming Languages in the US. Links Francille's LinkedIn TTFA Mentorship Program TTFA Merch Store TTFA Patreon TTFA Ko-Fi

    1h 36m

  4. 10/27/2025

    #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 leading german blog on functional programming. Member of the Editorial Board of the JFP. Part of the R6RS, the 6th revised report on the Algorithmic Language Scheme. In our conversation we talk about C, Lisp, Emacs Lisp, Scheme and his involvement with the R6RS. His views on mathematics and formal methods as languages, his views on the use of Functional Programming in the Industry, his thoughts of how Object Oriented Programming is dead. Macros, hygienic macros and much more! We also talk about BobKonf and FunArch as amazing confereces on Functional Programming and their design and archtechture. BobKonf currently has a call for talks open and goes until november 17th. Consider supporting the show! TTFA Patreon One time donations Merch Store Links Mike's Website Bob Konf FunArch Functional Programming Blog TTFA Graduate Mentorship

    2h 38m

  5. 09/29/2025

    #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 Stanford, his Masters in 1979 and his PhD in 1984 both at CMU. In 2023, he was awarded the distinguished honor of being elected a Fellow of the Royal Society, joining the ranks of scientific greats such as Isaac Newton and Charles Darwin. Wadler describes himself as someone who likes to bring theory into practice, and practice into theory. In this episode, we talk about his prolific research, the story behind Monads and Type Classes, Category Theory and Homotopy Type Theory. Throughout our conversation, in response to my eagerness to understand the philosophy and method behind his remarkable papers, he repeatedly emphasizes that the whole point of science is clearly communicating ideas so that others can build upon them. Links Wadler's Website Ullman's Advising Students For Success Grad School Mentorship Consider contributing to this show through our ko-fi!

    1h 50m

  6. 08/27/2025

    #53 RustBelt, Iris, and the Art of Writing - Derek Dreyer

    Derek Dreyer is a professor at the Max Planck Institute, in 2024 he was awarded the ACM Fellowship, in 2017 he got the ACM Sigplan Robin Milner Young Researcher Award. And has participated or lead greatly influential work, such as the RustBelt Project and Iris. In this episode Derek shares his experience going to Grad School at CMU, how even a great research as himself has fallen pray to the impostor syndrome and how to cope with it. Throughout the conversation he makes beautiful parallels between music and academic papers, and how the work of a researcher is similar to that of an artist an many aspects. He also gives us a few tips about how to become a better academic writer. And of course, we also talked about Rust and the history about formally verifying its type system. Don't forget to check our merch store! Links Derek's Website POPL '25 PLMW Talk - How to Write Papers so that People Can Read Them

    2h 25m

  7. 07/10/2025

    #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 back in 1984, and was behind HBC, the first publicly available Haskell compiler. If you've used Haskell, worked with hardware described in Bluespec, or played around with weird combinator-based toy languages, there's a decent chance you've crossed paths with his ideas — directly or indirectly. He's also won the International Obfuscated C Code Contest — not once, but multiple times — reminding us that playfulness and rigor aren't mutually exclusive. But his work didn't stop in academia or hobby projects. He’s brought functional programming into finance, hardware design, large-scale industry — with stints at Credit Suisse, Facebook, Google, and now Epic Games, where he’s helping design a new functional logic programming language called Verse. Over the course of this conversation, we’ll talk about lazy evaluation, type theory, programmable dungeons, the compromises of real-world programming, and what it means to still be building languages after 40 years in the game. Links Type Theory Forall Merch Store Ko-Fi Discord Server Haskell Interlude Lennart's Wikipedia Page Lennart's Webpage

    1h 31m

  8. 06/04/2025

    #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 rebranding from Coq into Rocq, which is very exciting to our community. However, Nicolas has such a prolific research career that I couldn’t miss the opportunity to get him to talk so much more about it. So in this conversation we talk about his early publications in neuroscience, his views on Category Theory applied to Type Theory, Rocq’s rebranding, and the institution around it, MetaRocq and the conceptual boundaries of certifying a theory inside itself. Of course we wouldn’t miss the opportunity to also discuss how Rocq view the growing influence that Lean is gaining in our community. Links Type Theory Forall Store Type Theory Forall Website Nicolas Tabareau Website MetaRocq Github

    1h 42m
See All (70)

Ratings & Reviews

4.8
out of 5
13 Ratings

About

An accessible podcast about Type Theory, Programming Languages Research and related topics.

Information

  • Creator
    Pedro Abreu
  • Years Active
    2020 - 2025
  • Episodes
    70
  • Rating
    Explicit
  • Copyright
    © CC BY 4.0
  • Show Website
    Type Theory Forall

You Might Also Like