Latest Type theory Podcast Episodes
#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen
Type Theory Forall - June 13, 2024 20:30 - 1 hour ★★★★★ - 6 ratingsIn 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’...
Turing's proof of normalization for STLC
Iowa Type Theory Commute - May 21, 2024 03:00 - 17 minutes ★★★★★ - 13 ratingsIn this episode, I describe the first proof of normalization for STLC, written by Alan Turing in the 1940s. See this short note for Turing's original proof and some historical comments.
#38 Haskell, Lean, Idris, and the Art of Writing - David Christiansen
Type Theory Forall - May 16, 2024 21:30 - 1 hour ★★★★★ - 6 ratingsIn 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...
Introduction to normalization for STLC
Iowa Type Theory Commute - May 14, 2024 04:00 - 9 minutes ★★★★★ - 13 ratingsIn this episode, after a quick review of the preceding couple, I discuss the property of normalization for STLC, and talk a bit about proof methods. We will look at proofs in more detail in the coming episodes. Feel free to join the Telegram group for the podcast if you want to discuss anythin...
The curious case of exponentiation in simply typed lambda calculus
Iowa Type Theory Commute - May 04, 2024 14:00 - 7 minutes ★★★★★ - 13 ratingsLike addition and multiplication on Church-encoded numbers, exponentiation can be assigned a type in simply typed lambda calculus (STLC). But surprisingly, the type is non-uniform. If we abbreviate (A -> A) -> A -> A as Nat_A, then exponentiation, which is defined as \ x . \ y . y x, can be as...
Arithmetic operations in simply typed lambda calculus
Iowa Type Theory Commute - May 04, 2024 14:00 - 9 minutes ★★★★★ - 13 ratingsIt is maybe not so well known that arithmetic operations -- at least some of them -- can be implemented in simply typed lambda calculus (STLC). Church-encoded numbers can be given the simple type (A -> A) -> A -> A, for any simple type A. If we abbreviate that type as Nat_A, then addition and ...
More on basics of simple types
Iowa Type Theory Commute - April 29, 2024 15:00 - 15 minutes ★★★★★ - 13 ratingsI review the typing rules and some basic examples for STLC. I also remind listeners of the Curry-Howard isomorphism for STLC.
Begin Chapter on Simple Type Theory
Iowa Type Theory Commute - April 19, 2024 16:00 - 15 minutes ★★★★★ - 13 ratingsIn this episode, after a pretty long hiatus, I start a new chapter on simply typed lambda calculus. I present the typing rules and give some basic examples. Subsequent episodes will discuss various interesting nuances...
#37 Compilers, Staging, Futamura Projections - Guannan Wei
Type Theory Forall - March 11, 2024 18:30 - 1 hour ★★★★★ - 6 ratingsIn 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 P...
#36 Behind the Person Behind this Podcast - Pedro Abreu
Type Theory Forall - December 26, 2023 15:00 - 1 hour ★★★★★ - 6 ratingsIn 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 li...
#35 Teika, Self-Education and F***ing Floating Points - Eduardo Rafael
Type Theory Forall - December 04, 2023 11:30 - 1 hour ★★★★★ - 6 ratingsIn 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...
#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke
Type Theory Forall - October 16, 2023 12:10 - 1 hour ★★★★★ - 6 ratingsAndrew 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 Websi...
Some advanced examples in DCS
Iowa Type Theory Commute - September 25, 2023 03:00 - 23 minutes ★★★★★ - 13 ratingsThis episode presents two somewhat more advanced examples in DCS. They are Harper's continuation-based regular-expression matcher, and Bird's quickmin, which finds the least natural number not in a given list of distinct natural numbers, in linear time. I explain these examples in detail and t...
DCS compared to termination checkers for type theories
Iowa Type Theory Commute - September 19, 2023 03:00 - 19 minutes ★★★★★ - 13 ratingsIn this episode, I continue introducing DCS by comparing it to termination checkers in constructive type theories like Coq, Agda, and Lean. I warmly invite ITTC listeners to experiment with the tool themselves. The repo is here.
Getting started with DCS
Iowa Type Theory Commute - September 10, 2023 04:00 - 17 minutes ★★★★★ - 13 ratingsIn this episode, I talk more about the DCS tool, and invite listeners to check it out and possibly contribute! The repo is here.
#33 Z3 and Lean, the Spiritual Journey - Leo de Moura
Type Theory Forall - September 09, 2023 14:40 - 2 hours ★★★★★ - 6 ratingsNot 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...
Introduction to DCS
Iowa Type Theory Commute - September 04, 2023 04:00 - 11 minutes ★★★★★ - 13 ratingsDCS is a new functional programming language I am designing and implementing with Stefan Monnier. DCS has a pure, terminating core, around which monads will be layered for possibly diverging, impure computation. In this episode, I talk about this basic design, and its rationale.
Semantics of subtyping
Iowa Type Theory Commute - July 24, 2023 03:00 - 15 minutes ★★★★★ - 13 ratingsI answer a listener's question about the semantics of subtyping, by discussing two different semantics: coercive subtyping and subsumptive subtyping. The terminology I found in this paper by Zhaohui Luo; see Section 4 of the paper for a comparison of the two kinds of subtyping. With coercive s...
#32 TyDe Systems - Jan de Muijnck-Hughes
Type Theory Forall - July 22, 2023 15:50 - 1 hour ★★★★★ - 6 ratingsIn 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 ...
More on type inference for simple subtypes
Iowa Type Theory Commute - July 16, 2023 02:00 - 9 minutes ★★★★★ - 13 ratingsI continue the discussion of Mitchell's paper Type Inference with Simple Subtypes. Coming soon: a discussion of semantics of subtyping.
#31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes
Type Theory Forall - July 13, 2023 15:20 - 2 hours ★★★★★ - 6 ratingsIn 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 ...
Subtyping, the golden key
Iowa Type Theory Commute - July 09, 2023 03:00 - 9 minutes ★★★★★ - 13 ratingsIn this episode, I wax rhapsodic for the potential of subtyping to improve the practice of pure functional programming, in particular by allowing functional programmers to drop various irritating function calls that are needed just to make types work out. Examples are lifting functions with mon...
Type inference with simple subtypes
Iowa Type Theory Commute - June 30, 2023 04:00 - 13 minutes ★★★★★ - 13 ratingsIn this episode, I begin discussing a paper titled "Type Inference with Simple Subtypes," by John C. Mitchell. The paper presents algorithms for computing a type and set of subtype constraints for any term of the pure lambda calculus. I mostly focus here on how subtype constraints allow typing...
Basics of subtyping
Iowa Type Theory Commute - June 21, 2023 21:00 - 8 minutes ★★★★★ - 13 ratingsIn this episode, I discuss a few of the basics for what we expect from a subtyping relation on types: reflexivity, transitivity, and the variances for arrow types.
Begin chapter on subtyping
Iowa Type Theory Commute - June 21, 2023 03:00 - 16 minutes ★★★★★ - 13 ratingsWe begin a discussion of subtyping in functional programming. In this episode, I talk about how subtyping is a neglected feature in implemented functional programming languages (for example, not found in Haskell), and how it could be very useful for writing lighter, more elegant code. I also t...
#30 Actors, GADTs and Burnout - Dan and Pedro
Type Theory Forall - May 30, 2023 23:30 - 1 hour ★★★★★ - 6 ratingsIn 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 GAD...
Last episode discussing Observational Equality Now for Good
Iowa Type Theory Commute - April 13, 2023 05:00 - 12 minutes ★★★★★ - 13 ratingsIn this episode, I conclude my discussion of some (but hardly all!) points from Pujet and Tabareau's POPL 2022 paper, "Observational Equality -- Now for Good!". I talk a bit about the structure of the normalization proof in the paper, which uses induction recursion. See this paper by Peter Dyb...
#29 Can PL theory make you a better software engineer? - Jimmy Koppel
Type Theory Forall - April 09, 2023 21:30 - 1 hour ★★★★★ - 6 ratingsJimmy 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! Lin...
More on observational type theory
Iowa Type Theory Commute - March 23, 2023 05:00 - 13 minutes ★★★★★ - 13 ratingsI continue discussing the Puject and Tabareau paper, "Observational Equality -- Now for Good", in particular discussing more about how the equality type simplifies based on its index (which is the type of the terms being equated by the equality type), and how proofs of equalities can be used to ...
Introduction to Observational Type Theory
Iowa Type Theory Commute - March 06, 2023 05:00 - 10 minutes ★★★★★ - 13 ratingsIn this episode, I introduce an important paper by Pujet and Tabareau, titled "Observational Equality: Now for Good", that develops earlier work of McBride, Swierstra, and Altenkirch (which I will cover in a later episode) on a new approach to making a type theory extensional. The idea is to ha...
Related Type theory Topics