Introduction to normalization for STLC

Update: 2024-05-14

Description

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 aaron.stump@gmail.com).

Comments

In Channel

Measure Functions and Termination of STLC

2025-11-1421:42

Schematic Affine Recursion, Oh My!

2025-08-2218:49

The Stunner: Linear System T is Diverging!

2025-08-1921:03

Terminating Computation First?

2025-08-0111:27

Correction: the Correct Author of the Proof from Last Episode, and an AI flop

2025-05-1207:10

Krivine's Proof of FD, Using Intersection Types

2025-05-0521:35

A Measure-Based Proof of Finite Developments

2025-04-1623:24

Introduction to the Finite Developments Theorem

2025-03-2715:54

Nominal Isabelle/HOL

2025-01-3116:18

The Locally Nameless Representation

2025-01-0319:54

POPLmark Reloaded, Part 2

2024-12-2313:59

POPLmark Reloaded, Part 1

2024-12-2315:14

Introduction to Formalizing Programming Languages Theory

2024-11-2512:20

Turing's proof of normalization for STLC

2024-05-2117:39

Introduction to normalization for STLC

2024-05-1409:39

The curious case of exponentiation in simply typed lambda calculus

2024-05-0407:29

Arithmetic operations in simply typed lambda calculus

2024-05-0409:56

Introduction to normalization for STLC

#box-pro-ellipsis-176436538194090{-webkit-line-clamp:2;}Introduction to normalization for STLC

Introduction to normalization for STLC

Aaron Stump

Introduction to normalization for STLC