#51 s/Coq/Rocq - Nicolas Tabareau Jun 04, 2025

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

#50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra May 14, 2025

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

Discount code for 10% off: typetheory

#49 Self-Education in PL - Ryan Brewer Mar 14, 2025

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, and Arctic.

In this episode we will talk about all of his projects. His trajectory becoming self-taught in PL, compilers and Formal Methods, and he shares with us the wealth of resources he used to navigate this sea of knowledge. We also have a brief but heated discussion on the ethics of Science.

0:00 – Intro & Podcast Community 3:40 – How Ryan Started Learning Programming Languages 12:40 – Projects, Category Theory & Early Experiences 18:00 – College Life, Dropping Out & Study Strategies 27:00 – Landing a Developer Job Without a Degree 32:00 – Thoughts on JavaScript, TypeScript & WebAssembly 37:00 – Building Arctic: A Compiler for Blogs 41:00 – Introduction to Gleam & Its Unique Features 48:00 – Functional Programming at Work & Community Impact 59:00 – Diving into Haskell and Category Theory 1:08:30 – Ethical Considerations in Software Licensing 1:20:00 – Reflections on Academia & Learning 1:32:30 – Job Interviews & Practical Programming Tools 1:38:00 – Dan on Academia and Podcasting Philosophy 1:54:00 – Final Reflections & Advice for Self-Learners 2:05:00 – Closing Thoughts, Blog, Open Source 2:19:58 – Outro

Links

#48 Bell Labs - David MacQueen Jan 21, 2025

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

#47 The History of LCF, ML and HOPE - David MacQueen Jan 07, 2025

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

#46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie Pédrot Nov 29, 2024

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

#45 What is Type Theory and What Properties we Should Care About - Pierre-Marie Pédrot Nov 24, 2024

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

#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro Nov 06, 2024

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/typetheoryforall

Links

#43 PL in the Industry and Summer Schools - Patrick and Eric Sep 13, 2024

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 doing some cool functional programming and formal methods. Before that we were pals doing an internship at Galois, and even before that he finished his masters with Benjamin Delaware at Purdue, Patrick’s current advisor. Patrick has just returned from his internship at AWS in the automated reasoning team. So in this episode we talk about their research, their academic and industry experiences, how’s the industry looking like for opportunities in PL and all that.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

#42 Distributed Systems, Microservices, and Choreographies - Fabrizio Montesi Aug 29, 2024

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 calculi that model distributed systems, their type systems, their Curry-Howard correspondences, and all the main ideas around these concepts.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links

#41 The Value of PL (and) Education - Satnam Singh Aug 15, 2024

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 works at Groq, applying FP to design silicon for machine learning. In this episode we talk about the value of specification, the current state of academia, gaming the metrics, functional programming in hardware, bullying, among other things.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links

#40 Secure Voting - Joe Kiniry Jul 15, 2024

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 tirelessly in designing, developing, supporting and auditing all kinds of voting systems for different private parties and government parties.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links

#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen Jun 13, 2024

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 Little Typer together with Dan Friedman, and we get more technical by talking about Equality, Bidirectional Type Checking, Quotation and Quasi Quotation.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links:

#38 Haskell, Lean, Idris, and the Art of Writing - David Christiansen May 16, 2024

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 about Functional Programming Writing and Dependent Types, and we still wouldn’t run out of topics!

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

#37 Compilers, Staging, Futamura Projections - Guannan Wei Mar 11, 2024

In this episode we talk with Guannan Wei, from Purdue University. Guannan finished his PhD last year under Tiark Rompf, and is currently doing his Post-Doc with Tiark. Guannan has worked on a plethora of different compilers topics, and in this conversation we will talk about Staging, Futamura Projections, Symbolic Execution, Compiler Applications in Smart Contracts and Quantum Programming. Towards the end of the episode we also talk about his application experiences for the position of a Professorship in the US an a few other contries.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links

#36 Behind the Person Behind this Podcast - Pedro Abreu Dec 26, 2023

In this episode we celebrate 3 years of existence of this podcast by reflecting on the journey so far, what is my philosophy, how do I approach the interviews, my overall goals for the show, and some of our plans for the future.

In order to achieve this, I first take a detour and tell you a little more about my personal history, and my carreer in type theory and programming languages.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

#35 Teika, Self-Education and F***ing Floating Points - Eduardo Rafael Dec 04, 2023

In this episode we talk with Eduardo Rafael. He is self-thaught programming languages enthusiast, youtuber, twitch streamer, multi-skilled programmer that has worked in different aspects of computer science such as PL, operating systems, blockchain, and many other stuff. In this conversation we talk about his experience as a developer and hacker that didn’t follow the conventional paths of going to school and what are the strategies to navigate the vast ocean of knowledge without guidance of teachers or institutions.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links

#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke Oct 16, 2023

Andrew Marmaduke is a PhD Candidate from the University of Iowa, he works under Aaron Stump and has been working on revamping the theorem prover Cedille 2. In this episode we tackle fundamental questions about the foundations of the theorem provers, Cedille and Cedille 2.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links

#33 Z3 and Lean, the Spiritual Journey - Leo de Moura Sep 09, 2023

Not satisfied with implementing one of the most popular automated theorem provers, Z3, Leo de Moura also tackles another extremely hard problem in our field and implements a brand new interactive theorem prover from scratch, Lean. In this episode we dive into the mind and philosophy of this man.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links

#32 TyDe Systems - Jan de Muijnck-Hughes Jul 22, 2023

In this episode we continue our conversation with Jan de Muijnck-Hughes a Research Associate at Glasgow University. He works using all sorts of fancy type systems mostly targeted for hardware specification, particularly with the aid of the theorem prover Idris. This episode we start by talking a little about Impostor Syndrome in academia and how he has learned to cope with it and then we dive deeper into the technicalities of his research, in particular his philosophy on Type Directed Design of Systems. We talk about Session Types, Graded Types, Quantitative types, etc.

Don't forget to join our new discord channel!

If you like our show please consider donating any amount at ko-fi.

Links

Project Pages

Cool People

Software

#31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes Jul 13, 2023

In this episode we have a deep conversation with Jan de Muijnck-Hughes, talks about all the cool research he has done with idris, hardware and different kinds of interesting type systems such as session types, quantitative types and graded types. In the second half we discuss all the different kinds of problems that has been going on in PL academia lately and what we can do as a community to address those issues.

Also, we have a discord channel now, join us!

If you like our show please consider donating any amount at ko-fi.

Errata:

Jan mentions 'Jeff Foster' when, in fact, he meant Nate Foster
This is the SIGCOMM 'Call': https://sigcomm.quest/
Felinne Hermans did her PhD at Eindhoven and not Delft

Links

Project Pages

Cool People

Software

#30 Actors, GADTs and Burnout - Dan and Pedro May 30, 2023

In this episode we have over Dan Plyukhin, a PhD Candidate from the University of Illinois Urbana-Champaign.

We talk about Dan’s research is in the field of parallelism, more specifically 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 to take 10 months off from his PhD to be with his family back in Brazil.

Links

#29 Can PL theory make you a better software engineer? - Jimmy Koppel Apr 09, 2023

Jimmy Koppel, got his PhD at MIT and found the Mirdin Company, where he teaches engineers to write better code! In this interview we talk about how to make better code, how the knowledge of computer science theory and programming languages can help engineers to achieve that, and much more!

Links

Newsletters discussed in the show

#28 Formally Verifying Smart Contracts - Pruvendo Feb 15, 2023

In this episode we host another company that does formal method in the context 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

#27 Formalizing an OS: The seL4 - Gerwin Klein Feb 04, 2023

In this episode talk with Gerwin Klein about the formal verification of the microkernel seL4 which was done using Isabelle at NICTA / Data61 in Australia. We also talk a little about his PhD Project veryfing a piece of the Java Virtual Machine.

Links

#26 Mechanizing Modern Mathematics - Kevin Buzzard Jan 16, 2023

Kevin Buzzard has been very passionate spreading the word among mathematicians to use theorem provers mechanize theorems of modern mathematics. In this conversation we will talk about his vision in teaching undergrads to use the Lean theorem prover, what is the Xena Project, his view of how theorem provers can change the way we do mathematics, and much more!

Links

#25 Formally Verifying the Tezos Codebase - Formal Land Nov 21, 2022

In this episode we partner with Formal Land, a company that works in formally verifying the Tezos codebase! I have worked with them in the past developing new features to their source-to-source compiler CoqOfOcaml. In this episode we talk about their work with Tezos and how their techniques are applicable to other codebases as well! For this we talk with Formal Land founder Guillaume Claret and the proof engineers Daniel Hilst and Pierre Vial.

Links

Formal Land Website
Formal Land Email: contact@formal.land
Formal Land Twitter: @LandFooBar
CoqOfOcaml
The DAO hack

#24 The History of Isabelle - Lawrence Paulson Oct 06, 2022

In this episode we interview Lawrence Paulson, one of the creating fathers of Isabelle.

We talk about the development process, how it drew inspirations and ideas from LCF and Boyer Moore. What tools were used, it’s strenghts and weaknesses, and all about the historical context at the time! We also briefly talk about his formalization of the Gödel's Incompletenes theorems in Isabelle

Paulson have quite an extensive CV, he is a professor at Cambridge, have published more than 100 papers, is an ACM fellow since 2008, is a member of the royal society since 2017, among many other things!

Links

#23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich Sep 24, 2022

In this episode we talk about Sigplan, the organization behind the most important conferences and proceedings in our field. What is the SIGPLAN? What exactly does it do? How is it organized? How are things published? To answer these and many other questions we talk with Jens Palsberg, a professor at UCLA, who is the past chair of the SIGPLAN. And also Jonathan Aldrich, a professor at the CMU, who is a member of the ACM publication board.

Links

#22 Impredicativity, LEM, Realizability and more - Cody Roux Aug 12, 2022

In this episode Cody Roux teaches some interesting concepts that people care about in Mathematics and Logic as a way to try to understand what is going on in the universe around us! In particular we will try to explain concepts such as Impredicativity, Excluded Middle, Group Theory, Model Theory, Kripke Models, Realizability, The Markov Principle, Cut Elimination, and other stuff!

Links

#21 Denotational Design - Conal Elliott Aug 04, 2022

In this episode Conal Elliott gives a more concrete presentation on 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 philosophical conversation to explain why he believes that Denotational Design is a superior form of reasoning in the realm of computer science.

We also continue a discussion raised by Dan Ghica on the last episode on the need for Operational Semantics and the role of elegance in reasoning and design.

Along the way we also address the questions sent by the listeners in these last episodes.

Links

Quotes

"A theory appears beautiful or elegant [...] when it’s simple; in other words when it can be expressed very concisely in terms of mathematics that we’ve already learned for some other reasons." - Murray Gell-Mann, Beauty and Elegance in Physics.
"In Galileo’s time, professors of philosophy and theology—the subjects were inseparable—produced grand discourses on the nature of reality, the structure of the universe, and the way the world works, all based on sophisticated metaphysical arguments. Meanwhile, Galileo measured how fast balls roll down inclined planes. How mundane! But the learned discourses, while grand, were vague. Galileo’s investigations were clear and precise. The old metaphysics never progressed, while Galileo’s work bore abundant, and at length spectacular, fruit. Galileo too cared about the big questions, but he realized that getting genuine answers requires patience and humility before the facts." - Frank Wilczek, (The Lightness of Being: Mass, Ether, and the Unification of Forces)
"We must make here a clear distinction between belief and faith, because, in general practice, belief has come to mean a state of mind which is almost the opposite of faith. Belief, as I use the word here, is the insistence that the truth is what one would ‘lief’ or wish it to be. The believer will open his mind to the truth on the condition that it fits in with his preconceived ideas and wishes. Faith, on the other hand, is an unreserved opening of the mind to the truth, whatever it may turn out to be. Faith has no preconceptions; it is a plunge into the unknown. Belief clings, but faith lets go. In this sense of the word, faith is the essential virtue of science, and likewise of any religion that is not self-deception." - Alan Watts (The Wisdom of Insecurity: A Message for an Age of Anxiety)

#20 Huaweii, String Diagrams, Game Semantics - Dan R. Ghica Jun 28, 2022

In this episode, me and Eric Bond have a great conversation with Dan R. Ghica, a professor at Birmingham University and Director of the Programming Language Research Lab of the Huaweii Research Centre Edinburgh. We talk about his work on both institutions, which includes topics such as Category Theory, String Diagrams, and Game Semantics. We also briefly discuss the current publication process of our field and entertain some thoughts on how to make it better. Finally, we touch on more personal topics such as his views about Elegance, making an insightful counterpoint to Conal’s opinions on Denotational Semantics vs. Operational Semantics.

Links

Talks and Lectures

Papers

Links

#17 The Lost Elegance of Computation - Conal Elliott May 09, 2022

In this episode I had the pleasure to have an in-depth conversation with Conal Elliott about his life, his work, his philosophy and his many opinions about research and the current state of PL Research and how it lead him to come with the concept of Denotational Design. Conal got his PhD at CMU in the 90s under Frank Pfenning working on Higher-Order Unification, after that he has devoted his life on thinking and refining graphic computation and the tools behind it.

Links

Conal's website
Play/work with Conal
Conal's twitter: @conal
The simple essence of automatic differentiation
Compiling to categories
Generic parallel functional programming
Denotational design with type class morphisms
Functional Images
Functional Reactive Animation
Alphabet Versus the Goddess - Leonard Shlain
The information - James Gleick
Murray Gell-Mann’s definition of beauty/elegance: "A theory appears beautiful or elegant [...] when it’s simple; in other words when it can be expressed very concisely in terms of mathematics that we’ve already learned for some other reasons."
A John Backus quote (from his Turing Award lecture): “Many creative computer scientists have retreated from inventing languages to inventing tools for describing them. Unfortunately, they have been largely content to apply their elegant new tools to studying the warts and moles of existing languages. After examining the appalling type structure of conventional languages, using the elegant tools developed by Dana Scott, it is surprising that so many of us remain passively content with that structure instead of energetically searching for new ones.”

#16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx Apr 02, 2022

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, the Uniqueness of Identity of Proofs, UIP for short, and why it is inconsistent with Homotopy Type Theory.

Links

Jesper's Website
Jesper's Twitter: @agdakx
Jesper's PhD Thesis
Rewrite Theory paper
Pattern matching without K paper (Check his website for more)
EuroProofNet
WITS Talks on Youtube (Workshop on the Implementation of Type Systems)
Agda Zulip
Agda Mailing List
Ataca Github
Wadler's book on Agda
Stump's book on Agda

#15 Coq Projects, Agda, Idris, Kind - Nitin and Eric Mar 27, 2022

In this episode me, Eric and Nitin continues our conversation started in the last episode. This time we move our attention to the cool projects happening in Coq, in particular commenting through the projects mentioned in Andrew Appel’s keynote “Coq’s Vibrant Ecosystem for verification engineering” that took place in CPP’22 which is colocated with POPL and towards the end we also talk about agda, idris and Kind.

Links

#14 POPL, Parametricity, Scala, DOT - Nitin and Eric Feb 12, 2022

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
Reynolds Paper
Practical Foundations for Programming Languages

#13 C/C++, Emacs, Haskell, and Coq. The Journey - John Wiegley Dec 23, 2021

This episode is about the journey of a programmer that converted himself into a 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 make him learn Coq and Category Theory?
How does Coq compare with ACL2?
How do both Coq and ACL2 compares to TLA+?
Did learning Coq make John a better programmer?

Links

John's Email: johnw@newartisans.com
John's Twitter: @jwiegley

#12 Tenure, Sexism and ADHD - Talia Ringer Nov 10, 2021

Talia Ringer is an Assistant Professor at University of Illinois Urbana-Champaign. She did her PhD at University of Washington with her thesis on Proof Repair.

She’s very active on twitter @taliaringer. And in this episode we will talk about her transition from PhD to Professor, her work on diversity, her ADHD and how it has affected her career so far, and we also touch on the delicate topic of sexism in academia.

Links

#11 FP, Monads, GHC, and beyond - Alejandro Serrano Oct 04, 2021

In this episode we have talk with Alejandro Serrano Mena, he works on 47 degrees and is a published author of two books about Haskell: The Book of Monads and Practical Haskell.

We talk about many interesting features behind functional programming such as adts, pattern matching, impredicativity, monads, effects, hacking the ghc and how all this comes together to grab industry attention to adopt functional programming features over the past decade.

Links

#10 Classical Logic vs Intuitionistic Logic - Thorsten Altenkirch and Anupam Das Jul 15, 2021

In this episode we host a discussion between Anupam Das and Thorsten Altenkirch on the role of constructivism in mathematics, logic and computer science.

Anupam is a lecturer in the University of Birmingham in the UK, and Thorsten Altenkirch is a CS Professor at the University of Nottingham.

We discuss why constructive content in proofs matters, the law of excluded middle, the axiom of choice, category theory, and much more!

Links

#9 Logic and Proof Theory - Anupam Das May 28, 2021

#8 Cedille - Chris Jenkins May 11, 2021

In this episode I have a nice conversation with Chris Jenkins to talk about the 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 the typing rules fit one page. And yet it is strong enough to do relevant theorem proving. This is probably the most technical episode so far.

Links

#7 Hacking Isabelle's Internals - Dan Matichuk Apr 16, 2021

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 of Aarch32 Arm Archtecture at Galois.

#6 All The Dumb Questions on Gradual Types - Zeina Migeed Mar 29, 2021

In this episode we interview Zeina Migeed, a PhD Student at University of California Los Angeles, advised by Prof. Jens Palsberg

She Researches Gradual Types and had a paper published at POPL'20 named "What is Decidable about Gradual Types". here is a link to it

As the name of the episode suggests, I'll be asking her all the dumb questions related to not only gradual types, but also intersection types and recursive types as well!

#5 The History of Coq'Art - Yves Bertot Feb 27, 2021

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: yves.bertot@inria.fr

Affichage et manipulation interactive de formules mathématiques dans les documents structurés - Check figure 15 for an example on how Yves’ tools would build trees internally

A video showing his tool in practice, doing proofs with mouse clicks

A Genereic Approach to Building User Interfaces for Theorem Provers

#4 Theorem Provers, Functional Programming and Companies - Eric Bond Feb 15, 2021

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 consulting company on Functional Programming Languages, specially on Scala and Haskell. You can find Eric @ericbond10 on Twitter.

During the episode we mention PL Talks and the Midlands Graduate School in the Foundations of Computing Science 2021.

#3 ML for PL and Mental Health - Dan Zheng Feb 01, 2021

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 enhance each other. And towards the end we shift our attention to mental health, both in the academia and in the industry.

You can find Dan at twitter @dancherp

#2 Grad School Life - Rajan Walia and John Sarracino Jan 10, 2021

In this episode we host Rajan Walia and John Sarracino. Rajan is a last year PhD Student from Indiana University, working under Sam Tobin-Hochstadt. And John is a Postdoc working with Greg Morriset at Cornell University.

We talk about Grad School life, how academia life looks like, pressure to publish, work-life balance, industry vs academia, and much more!

Here you can find John’s Website. http://goto.ucsd.edu/~john/

And here is Matt Might’s website mentioned in the episode. http://matt.might.net/#blog

#1 What is PL research? - Prof. Ben Delaware Dec 23, 2020

In this episode we host Prof. Benjamin Delaware from Purdue University to discuss and try to answer some basic questions related to PL research:

What is PL research?

Why does it matter?

Why is it cool?

What is Lambda Calculus?

What is Type Theory?

Church-Turing Thesis?

Curry-Howard Correspondence?

What are proof assistants? Why are they cool?

Don’t forget to follow Ben on twitter @GhostofBendy

#0 Cool Internships in PL - Pedro Abreu Dec 14, 2020

Who is Pedro Abreu?

What is the goal of this Podcast?

What are My Research Interests?

In this episode I share about my internship experiences at Nicta (data61 now), Sifive, Galois and Nomadic Labs.

Welcome!

Don’t forget to checkout Galois’ new podcast hosted by Joey Dodds and Shpat Morina. Click Here

Our TOPPODCAST Picks

Follow Us

Stay Connected

Type Theory Forall

Links

Links

Links

Links

Links

Links

Links

Links

Links

Links

Links

Links:

Links

Links

Links

Links

Links

Project Pages

Cool People

Software

Links

Project Pages

Cool People

Software

Links

Links

Newsletters discussed in the show

Links

Links

Links

Links

Links

Links

Links

Links

Quotes

Links

Talks and Lectures

Papers

Other Links

Links

Links

Links

Links

Links

Links

Links

Links

Links

Links

Related Podcasts

1

2

3

4

5

6