Type Theory Forall

#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen

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

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

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!

#37 Compilers, Staging, Futamura Projections - Guannan Wei

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

#36 Behind the Person Behind this Podcast - Pedro Abreu

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.

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

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

#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke

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. Links Andrew's Website AndrasKovacs' Smalltt Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality Impredicative Encodings of (Higher) Inductive Types

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

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. Links Leo's Website Lean Z3 The Church of Logic Podcast

#32 TyDe Systems - Jan de Muijnck-Hughes

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

#31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes

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

#30 Actors, GADTs and Burnout - Dan and Pedro

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 Dan's Personal Website Twitter: @dplyukhn

#29 Can PL theory make you a better software engineer? - Jimmy Koppel

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 Jimmy's Personal Website Jimmy's Twitter Mirdin's Website Jimmy's Blog Lastest blog post One CFG-Generator to Rule Them All Automatically Deriving Control-Flow Graph Generators from Operatio...

#28 Formally Verifying Smart Contracts - Pruvendo

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 Pruvendo's Website Pruvendo's Linkdin Pruvendo's Twitter

#27 Formalizing an OS: The seL4 - Gerwin Klein

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 Gerwin's Twitter Gerwin's Website ProofCraft's Website

#26 Mechanizing Modern Mathematics - Kevin Buzzard

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 Xena's Project Twitter Xena Project's Website Lean's Website

#25 Formally Verifying the Tezos Codebase - Formal Land

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

#24 The History of Isabelle - Lawrence Paulson

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

#23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich

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 Jen's Website Jonathan's Website Jonathan's...

#22 Impredicativity, EM, Realizability and more - Cody Roux

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 Cody’s website Cody’s dblp

#22 Impredicativity, LEM, Realizability and more - Cody Roux

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 Cody's website Cody's dblp

#21 Denotational Design - Conal Elliott

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

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

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

#19 Experience Report: Learning Coq - Patrick and Supun

In today’s episode I invite two friends of mine Patrick Lafontaine and Supun Abeysinghe. We will talk about their experience learning Coq and we guide ourselves 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 with Rust. And Supun works more along the lines of machine learning in the context of systems.

#18 Gödel's Incompleteness Theorems - Cody Roux

In this episode Cody Roux talks about the Gödel's Incompleteness Theorems. We go through it’s underlying historical context, Hilbert’s Program, how it relates with 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's Theorems Jeremy Avigad's Lecture Notes

#17 The Lost Elegance of Computation - Conal Elliott

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

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

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

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

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 Nitin Twitter @NitinJohnRaj2 Eric Twitter @EricBond10 Appel's CPP Talk...

#14 POPL, Parametricity, Scala, DOT - Nitin and Eric

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

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

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

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

#12 Tenure, Sexism and ADHD - Talia Ringer

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 Talia's Twitter Sigplan Mentoring TIL: a type-directed, optimizi...

#11 FP, Monads, GHC, and beyond - Alejandro Serrano

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 Our new twitter @ttforall Alejandr...

#10 Classical Logic vs Intuitionistic Logic - Thorsten Altenkirch and Anupam Das

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 Thorsten's website Anupam's website Thorsten's Book on...

#9 Logic and Proof Theory - Anupam Das

#8 Cedille - Chris Jenkins

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 Leroy Jenkins Cedille Cast The Iowa Type Theory Commute Cedille Page Github Page

#7 Hacking Isabelle's Internals - Daniel Matichuk

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.

#7 Hacking Isabelle's Internals - Hacking Isabelle's Internals

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

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

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

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

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

#3 ML for PL and Mental Health - Dan Zheng

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

#2 Grad School Life - Rajan Walia and John Sarracino

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

#1 What is PL research? - Prof. Ben Delaware

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

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

#0 Cool Internships in PL - Believe or not there are quite a few companies interested in Programming Languages Research.

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