My journey of learning Lean 4 by implementing proofs from the wonderful book Programming Language Foundations in Agda.
- 1. Lambda: Introduction to Lambda Calculus
- 2. Properties: Progress and Preservation
- 3. DeBruijn: Intrinsically-typed de Bruijn representation
- 4. More: Additional constructs of simply-typed lambda calculus
- 5. Bisimulation: Relating reduction systems
- 6. Inference: Bidirectional type inference
- 7. Untyped: Untyped lambda calculus with full normalisation
- 8. Confluence: Confluence of untyped lambda calculus
- 9. BigStep: Big-step semantics of untyped lambda calculus
- 1. Denotational: Denotational semantics of untyped lambda calculus
- 2. Compositional: The denotational semantics is compositional
- 3. Soundness: Soundness of reduction with respect to denotational semantics
- 4. Adequacy: Adequacy of denotational semantics with respect to operational semantics
- 5. ContextualEquivalence: Denotational equality implies contextual equivalence
- 1. Substitution: Substitution in the untyped lambda calculus