Best Pedro Abreu Podcasts (2025)

1
#52 Why is Haskell so special - Lennart Augustsson 1:30:31

Play Pause

14d ago1:30:31

1:30:31

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 play…

1
#51 s/Coq/Rocq - Nicolas Tabareau 1:42:05

2M ago1:42:05

1:42:05

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 op…

1
#50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra 2:06:47

2M ago2:06:47

2:06:47

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 Haskel…

1
#49 Self-Education in PL - Ryan Brewer 2:23:47

4M ago2:23:47

2:23:47

Ryan 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 ivory tower of academia, and easier to put into practice where it matters. He has a couple of very interesting main projects, such as the first Cedille 2 Interpreter, Saber VM…

1
#48 Bell Labs - David MacQueen 2:10:12

6M ago2:10:12

2:10:12

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. …

1
#47 The History of LCF, ML and HOPE - David MacQueen 2:05:04

7M ago2:05:04

2:05:04

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 t…

1
#46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie Pédrot 1:03:36

8M ago1:03:36

1:03:36

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.…

1
#45 What is Type Theory and What Properties we Should Care About - Pierre-Marie Pédrot 1:21:41

8M ago1:21:41

1:21:41

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 …

1
#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro 2:13:31

9M ago2:13:31

2:13:31

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 provers, type systems properties, semantics and interoperabilities. If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/ty…

1
#43 PL in the Industry and Summer Schools - Patrick and Eric 1:01:30

10M ago1:01:30

1:01:30

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 pretty cool esoteric cubical agda stuff. Before starting his PhD he has spent some time at the consultancy companies Two Six Technologies and 47 Degrees …

1
#42 Distributed Systems, Microservices, and Choreographies - Fabrizio Montesi 1:52:49

11M ago1:52:49

1:52:49

In this episode we talk with Fabrizio Montesi, a Full Professor at the University of South Denmark. He is one of the creators of the Jolie Programming Language, President of the Microservices Community and Author of the book 'Introduction to Choreographies'. In today’s episode we talk about the formal side of Distributed Sytems, session types, the …

1
#41 The Value of PL (and) Education - Satnam Singh 1:41:04

11M ago1:41:04

1:41:04

Satnam Singh has got incredible experience in both academia and industry. He has worked in Google, Facebook, Microsoft, Microsoft Research, Xilinx, etc. He has been a lecturer in Glasgow, Birmingham and University of California for a couple of years. He has worked with many interesting tools such Coq, Haskell, Verilog, Tensorflow. These days he wor…

1
#40 Secure Voting - Joe Kiniry 1:08:54

1y ago1:08:54

1:08:54

In this episode we go into a deep dive into the formal methods side of Voting systems, and for this nobody better than our guest: Joe Kiniry, A Principal Scientist at Galois, Principled CEO and Chief Scientist of Free & Fair, a Galois spin-out focused on high-assurance elections technologies and services. For the past 20 years Joe has worked tirele…

1
#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen 1:49:42

1y ago1:49:42

1:49:42

In this episode we continue our conversation with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer. He has also worked as the Executive Director of the Haskell Foundation, at Galois and did his PhD developing a bunch of cool stuff for Idris. In today’s episode we talk about the story behind writing The Litt…

1
#38 Haskell, Lean, Idris, and the Art of Writing - David Christiansen 1:55:58

1y ago1:55:58

1:55:58

In this episode we talk with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer. He has also worked as the Executive Director of the Haskell Foundation, at Galois and did his PhD developing a bunch of cool stuff for Idris. David is a super upbeat person and I feel that we could spend hundreds of hours talking…

1
#37 Compilers, Staging, Futamura Projections - Guannan Wei 1:53:20

1+ y ago1:53:20

1:53:20

In this episode we talk with Guannan Wei, from Purdue University. Guannanfinished his PhD last year under Tiark Rompf, and is currently doing hisPost-Doc with Tiark. Guannan has worked on a plethora of differentcompilers topics, and in this conversation we will talk about Staging,Futamura Projections, Symbolic Execution, Compiler Applications in Sm…

1
#36 Behind the Person Behind this Podcast - Pedro Abreu 1:49:55

1+ y ago1:49:55

1:49:55

In this episode we celebrate 3 years of existence of this podcast byreflecting on the journey so far, what is my philosophy, how do Iapproach the interviews, my overall goals for the show, and some of our plansfor the future. In order to achieve this, I first take a detour and tell you a little moreabout my personal history, and my carreer in type …

1
#35 Teika, Self-Education and F***ing Floating Points - Eduardo Rafael 1:21:29

1+ y ago1:21:29

1:21:29

In this episode we talk with Eduardo Rafael. He isself-thaught programming languages enthusiast, youtuber, twitch streamer,multi-skilled programmer that has worked in different aspects of computerscience such as PL, operating systems, blockchain, and many other stuff. Inthis conversation we talk about his experience as a developer and hacker thatdi…

1
#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke 1:28:27

2y ago1:28:27

1:28:27

Andrew Marmaduke is a PhD Candidate from the University of Iowa, he worksunder Aaron Stump and has been working on revamping the theorem proverCedille 2. In this episode we tackle fundamental questions about thefoundations of the theorem provers, Cedille and Cedille 2. If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.…

1
#33 Z3 and Lean, the Spiritual Journey - Leo de Moura 2:05:07

2y ago2:05:07

2:05:07

Not satisfied with implementing one of the most popular automated theoremprovers, Z3, Leo de Moura also tackles another extremely hard problem inour field and implements a brand new interactivetheorem prover from scratch, Lean. In this episode we dive into the mind andphilosophy of this man. If you enjoy the show please consider supporting us at ou…

1
#32 TyDe Systems - Jan de Muijnck-Hughes 1:41:23

2y ago1:41:23

1:41:23

In this episode we continue our conversation with Jan de Muijnck-Hughes aResearch Associate at Glasgow University. He works using all sorts of fancytype systems mostly targeted for hardware specification, particularly withthe aid of the theorem prover Idris. This episode we start by talking alittle about Impostor Syndrome in academia and how he has…

1
#31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes 2:09:59

2y ago2:09:59

2:09:59

In this episode we have a deep conversation with Jan de Muijnck-Hughes, talksabout all the cool research he has done with idris, hardware and different kindsof interesting type systems such as session types, quantitative types and gradedtypes. In the second half we discuss all the different kinds of problems thathas been going on in PL academia lat…

1
#30 Actors, GADTs and Burnout - Dan and Pedro 1:44:52

2y ago1:44:52

1:44:52

In this episode we have over Dan Plyukhin, a PhD Candidate fromthe University of Illinois Urbana-Champaign. We talk about Dan’s research is in the field of parallelism, morespecifically garbage collection in the presence of actors. Then we also talk about Pedro's research on translating GADTs from OCaml to Coq,and the burnout process that lead him …

1
#29 Can PL theory make you a better software engineer? - Jimmy Koppel 1:24:19

2+ y ago1:24:19

1:24:19

Jimmy Koppel, got his PhD at MIT and found the Mirdin Company, where heteaches engineers to write better code! In this interview we talk about howto make better code, how the knowledge of computer science theory andprogramming languages can help engineers to achieve that, and much more! Links Jimmy's Personal Website Jimmy's Twitter Mirdin's Websit…

1
#28 Formally Verifying Smart Contracts - Pruvendo 1:10:40

2+ y ago1:10:40

1:10:40

In this episode we host another company that does formal method in thecontext of the Everscale Blockchain, and Solidity smart contracts.How and why they use formal methods in this context? Who are their clients?What are the caveats? Links Pruvendo's Website Pruvendo's Linkdin Pruvendo's TwitterBy Pedro Abreu

1
#27 Formalizing an OS: The seL4 - Gerwin Klein 1:58:40

2+ y ago1:58:40

1:58:40

In this episode talk with Gerwin Klein about the formal verification of themicrokernel seL4 which was done using Isabelle atNICTA / Data61 in Australia. We also talk a little about his PhD Projectveryfing a piece of the Java Virtual Machine. Links Gerwin's Twitter Gerwin's Website ProofCraft's Website…

1
#26 Mechanizing Modern Mathematics - Kevin Buzzard 2:15:31

2+ y ago2:15:31

2:15:31

Kevin Buzzard has been very passionate spreading the word amongmathematicians to use theorem provers mechanize theorems of modernmathematics. In this conversation we will talk about his vision in teachingundergrads to use the Lean theorem prover, what is the Xena Project, his viewof how theorem provers can change the way we do mathematics, and much…

1
#25 Formally Verifying the Tezos Codebase - Formal Land 1:01:32

2+ y ago1:01:32

1:01:32

In this episode we partner with Formal Land, a company that works in formallyverifying the Tezos codebase! I have worked with them in the past developingnew features to their source-to-source compiler CoqOfOcaml. In this episode wetalk about their work with Tezos and how their techniques are applicable toother codebases as well! For this we talk wi…

1
#24 The History of Isabelle - Lawrence Paulson 1:38:02

3y ago1:38:02

1:38:02

In this episode we interview Lawrence Paulson, one of the creating fathers ofIsabelle. We talk about the development process, how it drew inspirations andideas from LCF and Boyer Moore. What tools were used, it’s strenghts andweaknesses, and all about the historical context at the time! We also brieflytalk about his formalization of the Gödel's Inc…

1
#23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich 1:12:13

3y ago1:12:13

1:12:13

In this episode we talk about Sigplan, the organization behind the mostimportant conferences and proceedings in our field. What is the SIGPLAN? Whatexactly does it do? How is it organized? How are things published? To answerthese and many other questions we talk with Jens Palsberg, a professor atUCLA, who is the past chair of the SIGPLAN. And also …

1
#22 Impredicativity, LEM, Realizability and more - Cody Roux 2:19:23

3y ago2:19:23

2:19:23

In this episode Cody Roux teaches some interesting concepts that people careabout in Mathematics and Logic as a way to try to understand what is going onin the universe around us! In particular we will try to explain concepts suchas Impredicativity, Excluded Middle, Group Theory, Model Theory, KripkeModels, Realizability, The Markov Principle, Cut …

1
#21 Denotational Design - Conal Elliott 3:07:26

3y ago3:07:26

3:07:26

In this episode Conal Elliott gives a more concrete presentationon what is Denotational Design is and how to use it in practice. It is a continuation of episode #17, in which we had an in-depth philosophicalconversation to explain why he believes thatDenotational Design is a superior form of reasoning in the realm of computerscience. We also contin…

1
#20 Huaweii, String Diagrams, Game Semantics - Dan R. Ghica 1:37:28

3y ago1:37:28

1:37:28

In this episode, me and Eric Bond have a great conversation with Dan R.Ghica, a professor at Birmingham University and Director of the ProgrammingLanguage Research Lab of the Huaweii Research Centre Edinburgh.We talk about his work on both institutions, which includes topics such asCategory Theory, String Diagrams, and Game Semantics.We also briefl…

1
#19 Experience Report: Learning Coq - Patrick and Supun 1:51:39

3y ago1:51:39

1:51:39

In today’s episode I invite two friends of mine Patrick Lafontaine and SupunAbeysinghe. We will talk about their experience learning Coq and we guideourselves in a survey that I gave all the 83 students in the class.The class was thought by my advisor Benjamin Delaware and I was his TA. Patrick researches compilers and have done work in particular …

1
#18 Gödel's Incompleteness Theorems - Cody Roux 2:50:14

3y ago2:50:14

2:50:14

In this episode Cody Roux talks about the Gödel's Incompleteness Theorems. We gothrough it’s underlying historical context, Hilbert’s Program, how it relateswith Turing, Church, Von Neumann, Termination and more. Links Cody's website Cody's dblp The Lady or the Tiger? - Short Story The Lady or the Tiger? - Amazon Logicomix An Introduction to Gödel'…

1
#17 The Lost Elegance of Computation - Conal Elliott 3:32:38

3y ago3:32:38

3:32:38

In this episode I had the pleasure to have an in-depth conversation with ConalElliott about his life, his work, his philosophy and his many opinions aboutresearch and the current state of PL Research and how it lead him to come withthe concept of Denotational Design. Conal got his PhD at CMU in the 90s underFrank Pfenning working on Higher-Order Un…

1
#16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx 1:35:53

3+ y ago1:35:53

1:35:53

In this episode we interview Jesper Cockx, one of the core developers on Agda.We talk about the philosophy behind Agda, his work on pattern matching, theUniqueness of Identity of Proofs, UIP for short, and why it is inconsistentwith Homotopy Type Theory. Links Jesper's Website Jesper's Twitter: @agdakx Jesper's PhD Thesis Rewrite Theory paper Patte…

1
#15 Coq Projects, Agda, Idris, Kind - Nitin and Eric 1:17:36

3+ y ago1:17:36

1:17:36

In this episode me, Eric and Nitin continues our conversation started in thelast episode. This time we move our attention to the cool projects happeningin Coq, in particular commenting through the projects mentioned in AndrewAppel’s keynote “Coq’s Vibrant Ecosystem for verification engineering” thattook place in CPP’22 which is colocated with POPL …

1
#14 POPL, Parametricity, Scala, DOT - Nitin and Eric 56:30

3+ y ago56:30

56:30

In this episode I gather with two good friends Eric and Nitin to randomly talk random subjects that pops up. Among them we talked about POPL, Scala, Isabelle, Parametricity, Dependent Object Types (DOT, for short) and more! Links Nitin Twitter @NitinJohnRaj2 Eric Twitter @EricBond10 Collection of links on logical relations Theorems for Free Reynold…

1
#13 C/C++, Emacs, Haskell, and Coq. The Journey - John Wiegley 1:39:30

3+ y ago1:39:30

1:39:30

This episode is about the journey of a programmer that converted himself intoa Haskell developer after working with C/C++ for more than 10years. Here are a few questions that you'll find the answer to in this episode: What does he find so compelling about Haskell? Why did it make him dive deeper into the Theoretical Computer Science? Why did it mak…

1
#12 Tenure, Sexism and ADHD - Talia Ringer 1:05:53

3+ y ago1:05:53

1:05:53

Talia Ringer is an Assistant Professor at University of IllinoisUrbana-Champaign. She did her PhD at University of Washington with her thesison Proof Repair. She’s very active on twitter @taliaringer. And in this episode we will talkabout her transition from PhD to Professor, her work on diversity, her ADHD andhow it has affected her career so far,…

1
#11 FP, Monads, GHC, and beyond - Alejandro Serrano 1:07:12

4y ago1:07:12

1:07:12

In this episode we have talk with Alejandro Serrano Mena, heworks on 47 degrees and is a published author of two books about Haskell: TheBook of Monads and Practical Haskell. We talk about many interesting features behind functionalprogramming such as adts, pattern matching, impredicativity, monads, effects,hacking the ghc and how all this comes to…

1
#10 Classical Logic vs Intuitionistic Logic - Thorsten Altenkirch and Anupam Das 1:16:30

4y ago1:16:30

1:16:30

In this episode we host a discussion between Anupam Das and ThorstenAltenkirch on the role of constructivism in mathematics, logic and computerscience. Anupam is a lecturer in the University of Birmingham in the UK, and ThorstenAltenkirch is a CS Professor at the University of Nottingham. We discuss why constructive content in proofs matters, the l…

1
#9 Logic and Proof Theory - Anupam Das 57:20

4y ago57:20

57:20

By Pedro Abreu

1
#8 Cedille - Chris Jenkins 1:05:42

4y ago1:05:42

1:05:42

In this episode I have a nice conversation with Chris Jenkins to talk aboutthe Cedille theorem prover, based on a very concise type theory called CDLE.The main selling point of Cedille is that the theory is so small that thetyping rules fit one page. And yet it is strong enough to do relevant theoremproving. This is probably the most technical epis…

1
#7 Hacking Isabelle's Internals - Dan Matichuk 1:20:52

4+ y ago1:20:52

1:20:52

In this episode we dive into Isabelle, the interactive theorem prover based on Higher Order Logic directly from someone who spent quite some time hacking on its internals. Me and Daniel also talk about Mizar, Isar, the seL4, and how it is formalized. Torwards the end of the episode we also talk a little about his current work on the binary analysis…

1
#6 All The Dumb Questions on Gradual Types - Zeina Migeed 39:13

4+ y ago39:13

39:13

In this episode we interview Zeina Migeed, a PhD Student at University ofCalifornia Los Angeles, advised by Prof. Jens Palsberg She Researches Gradual Types and had a paper published at POPL'20 named "What isDecidable about Gradual Types". here is a link to it As the name of the episode suggests, I'll be asking her all the dumb questionsrelated to …

1
#5 The History of Coq'Art - Yves Bertot 1:11:46

4+ y ago1:11:46

1:11:46

In this episode we interview Yves Bertot and we talk about the history behind his contribution with Pierre Castéran on writing Coq’Art. What is Yves’ role in the Coq Team, how the team works and what are the sort of contributions they accept. Links: Yves email: [email protected] Affichage et manipulation interactive de formules mathématiques dan…

1
#4 Theorem Provers, Functional Programming and Companies - Eric Bond 1:14:23

4+ y ago1:14:23

1:14:23

In this episode we host Eric Bond to go through some real cool projects happening in the PL World and some of the companies behind them. We discuss some technical differences between the major interactive theorem provers out there, some of their most popular projects, and a few companies that work in the realm. Eric Bond works at 47 degrees, a cons…

1
#3 ML for PL and Mental Health - Dan Zheng 1:08:01

4+ y ago1:08:01

1:08:01

In this episode we host Dan Zheng, an alumni of Purdue University that now works at Google at real cool projects that relates ML and PL. We chat about how was his transition from undergrad to such a huge company like Google. We talk about cool languages such as Lantern, LLVM, LMS, Julia, Rust, Racket, Scala. How does ML and PL can be used to enhanc…