Strong Normalization of the Dependently Typed SK Combinators in Lean
In this repository, I define a dependent typing for the SK combinators, and prove strong normalization of this combinator calculus in Lean.
See the book for more.
Table of Contents
I aim for this repository to be relatively accessible to anyone who knows Lean or functional programming. A such, I assume little theoretical background knowledge. My hope is that this book gives you a good understanding of what strong normalization is, how it's proven, and how I've proven it for the dependently typed SK combinators--all in Lean.
- Background - provides an overview on typing, lambda calculus, and strong normalization
- Existing Work
- Type Discipline - in-depth technical details of how I represent dependent typings for the SK combinators
- Strong Normalization Proof - the proof
- Dependent SK - example demonstrating that these combinators are dependent