Lambda Calculus in Lean

 Lambda Calculus in Lean🔗

This book develops lambda calculi as object languages inside Lean. The chapters below are the actual Lean source files rendered as literate pages. The book is therefore a table of contents and publishing layer for the course files, not a second copy of their content.

Contents

  1. 1. Untyped Lambda Calculus: De Bruijn Terms
  2. 2. Named Terms
  3. 3. Confluence and Normal Forms
  4. 4. Simply Typed Lambda Calculus: Typing
  5. 5. Subject Reduction and Normal Forms
  6. 6. Building