Type Theory Forall

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!

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

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

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

Wouter Swierstra is a Math Bachelor’s from the University of Utrecht, has done his PhD with Thorsten Altenkirch at the University of Nottingham, did a post-doc at Chalmers, has experience in the industry working on facilitating the design of embedded system using FP and currently is a Professor at the University of Utrecht and co-host of the Haskell Interlude Podcast. In this episode we talk about his trajectory into formal methods and functional programming. We talk about Datatypes a la Carte, the Expression Problem, Functional Pearls, Program Synthesis vs Program Calculation, and much more! 0:00 – Intro & Welcome 0:02:08 – Announcing the Type Theory Forall Merch Store! 1:12 – Early Influences: From Lenses to Logic 4:40 – Discovering Functional Programming in Utrecht 8:15 – On Monads, Papers, and Learning by Teaching 12:20 – What Makes a Paper ‘Beautiful’? 17:50 – PhD in Nottingham: Theory Meets Community 22:00 – Writing ‘Certified Programming with Dependent Types’ 29:10 – Teaching Dependent Types: Challenges and Joys 34:00 – On Agda vs Coq: Philosophies and Use Cases 38:40 – Type-Driven Development in Practice 45:05 – The Power of Elegant Proofs 52:00 – Advice to Aspiring Researchers in Type Theory 1:03:00 – Beating C with Functional Programming 1:20:00 – Formal Verification and Loop Invariants 1:33:28 – Program Calculation vs Program Synthesis 1:39:00 – Formalizing Blockchain 2:01:38 – Final Thoughts Links Wouter Website Haskell Interlude Advanced FP Summer School ttforall twitch ttforall store Discount code for 10% off: typetheory

Ryan Brewer, a self-taught programming language expert and creator of innovative projects like Saber VM, shares his journey from college dropout to blog writer, dedicated to making formal theory accessible. Joined by researcher Dan Plukin, they discuss the challenges and joys of self-education in programming, the intersection of ethics and technology, and their experiences with compilers. They emphasize the importance of passion in learning and critique traditional academic paths, while encouraging openness in the programming community.

In this episode we continue with our conversation with David MacQueen, he is an Emeritus Professor from the University of Chicago, and has worked at Bell Labs for 20 years. Bell Labs began as the research and development section of the American Telephone and Telegraph company, aka AT&T, which originally hold exclusive hold of the telephone patent. Once that expired in the 1800s they needed to develop new technology to prove that it was still the best company, and hence Bell Labs was born. Over the course of the years this fascinating institution has registered more than 26 thousand patents, among of which we have the transistor, the laser, the solar cell and communication satellites. Over the course of the last 88 years they were awarded a jaw dropping amount of 10 Nobel prizes and 5 Turing awards. In this interview David MacQueen shares with us how was it like to work in such an incredible institution during it’s golden age. He shares insights about the technology, the space, the people, the management style, and much more! Links David's Website David's Github

David MacQueen has worked at Bell Labs for around 20 years during it’s Golden Age. Professor at Chicago University for 23 years. He is one of the designers of SML, one of the fathers of HOPE the programming language that introduced the notion of Algebraic Datatypes. So this interview was very special to me personally where I could get to hear all the stories about the dawn of Functional Programming as we know. And it is my great pleasure to have the honor to share it with you all. Links David's Website David's Github Luca Cardelli and the Early Evolution of ML The History of SML HOPE SML Website SML/NJ Website SML/NJ Github SML Family Website

In this episode Pierre-Marie Pédrot, one of the main Coq/Rocq developers joins us to talk about Krivine, Kleene and Gödel Realizability Models, how it relates to the BHK interpretation and CPS Translations, and how it was all already part of Gödel's work in Dialectica! If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall Links Pierre-Marie's Website Pierre-Marie's PhD Thesis (Very nice read) BHK Interpretation Type Theory Forall website Type Theory Forall discord

In this episode Pierre-Marie Pédrot who is one of the main Coq/Rocq developers joins us to talk about what is Type Theory, what is Martin-Löf Type Theory, what are the properties we should care about in our type theory and why. If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall Links Pierre-Marie's Website Type Theory Forall website Type Theory Forall discord