Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Podcasting since 2019 • 166 episodes
Iowa Type Theory Commute
Latest Episodes
Turing's proof of normalization for STLC
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 comment...
•
Season 5
•
Episode 6
•
17:39
Introduction to normalization for STLC
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...
•
Season 5
•
Episode 5
•
9:39
The curious case of exponentiation in simply typed lambda calculus
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...
•
Season 5
•
Episode 4
•
7:29
Arithmetic operations in simply typed lambda calculus
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 simpl...
•
Season 5
•
Episode 3
•
9:56