Iowa Type Theory Commute

May 20 2024 166 ep. 13 mins 146
Iowa Type Theory Commute Podcast artwork

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

  Technology  Science
RSS feed Share
Copy RSS


Subscribe on Podcast Addict


Turing's proof of normalization for STLC

May 20 2024 17 mins  
In 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.

Introduction to normalization for STLC

May 13 2024 9 mins  
In 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 anything (or just email me at [email protected]).

The curious case of exponentiation in simply typed lambda calculus

May 04 2024 7 mins  
Like 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 assigned type Nat_A -> Nat_(A -> A) -> Nat_A. The second argument needs to

Arithmetic operations in simply typed lambda calculus

May 04 2024 9 mins  
It 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 multiplication can both be typed in STLC, at type Nat_A -> Nat_A -> Nat_A.

More on basics of simple types

Apr 29 2024 15 mins  
I 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

Apr 19 2024 15 mins  
In 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...

Some advanced examples in DCS

Sep 24 2023 23 mins  
This 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 then discuss how they are implemented in DCS, which ensures that they are terminating on al

DCS compared to termination checkers for type theories

Sep 18 2023 19 mins  
In 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

Sep 09 2023 17 mins  
In this episode, I talk more about the DCS tool, and invite listeners to check it out and possibly contribute! The repo is here.

Introduction to DCS

Sep 03 2023 11 mins  
DCS 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.