Type Theory Forall
by Pedro Abreu
Latest episode
#65 TLA+, Quint and Formal Verification in the Age of AI - Gabriela…
#65 TLA+, Quint and Formal Verification in the Age of AI - Gabriela…
About this podcast
An accessible podcast about Type Theory, Programming Languages Research and
related topics.
Episodes
The newest 20 of 66 episodes
- #65 TLA+, Quint and Formal Verification in the Age of AI - Gabriela Moreira · 2 h 2 minHow 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…
- #64 PL Education in the Age of AI - Shriram Krishnamurthi · 2 h 43 minShriram 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…
- #63 Hack: Typing PHP at Facebook Scale - Julien Verlaguet · 1 h 46 minJulien is one of the creators of Hack, a language developed by Facebook to introduce types into PHP. In this episode he talks in depth about the semantics of PHP, and all the…
- #62 Dependent Haskell - Vladislav Zavialov · 2 h 4 minVlad works at Serokell to develop the Glasgow Haskell Compiler, he is a former member of the Haskell Steering Committee and the current implementer of Dependent Haskell. In this…
- #61 Zurihac Behind the Scenes - Farhad Mehta · 2 h 19 minIn this episode we talk with Farhad Mehta, one of the main organizers of Zurihac, the biggest Haskell event in the planet. Zurihac happens once a year at Zurich. This year’s…
- #60 Conversations on Life, AI, and the PL Job Market - Pedro and Dan · 1 h 53 minIn this episode me and Dan Plyukhin get together to have a heartfelt conversation. We start by talking about our experiences with meditation, and how it has helped us to have a…
- #59 Category Theory and Inclusivity - Valeria de Paiva · 2 h 46 minIn this episode of the Type Theory Forall podcast, we are joined by Valeria de Paiva, a Brazilian mathematician and logician whose work has had a lasting influence on category…
- #58 Constructivism and Computational Content - Andrej Bauer · 2 h 18 minAndrej 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…
- #57 Compilers for Privacy-Preserving Computation, Category Theory, and Keeping a Good Rythm in your PhD - Raghav Malik · 59 minRaghav 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…
- #56 Property Based Testing and PL Grad School Applications - Francille Zhuang · 1 h 36 minFrancille 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…
- #55 The Death of OO, The Beauty of Scheme, BobKonf, and FunArch - Mike Sperber · 2 h 38 minMike 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…
- #54 The Goal of Science is to Communicate Ideas! - Philip Wadler · 1 h 50 minPhilip 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…
- #53 RustBelt, Iris, and the Art of Writing - Derek Dreyer · 2 h 25 minDerek 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…
- #52 Why is Haskell so special - Lennart Augustsson · 1 h 30 minLennart 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…
- #51 s/Coq/Rocq - Nicolas Tabareau · 1 h 42 minIn 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…
- #50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra · 2 h 6 minWouter 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…
- #49 Self-Education in PL - Ryan Brewer · 2 h 23 minRyan Brewer is a college dropout who has an incredible blog about PL, Category Theory and Logic. He better define his goal as making Formal Theory more accessible outside the…
- #48 Bell Labs - David MacQueen · 2 h 10 minIn 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…
- #47 The History of LCF, ML and HOPE - David MacQueen · 2 h 5 minDavid 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…
- #46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie Pédrot · 1 h 3 minIn 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…
