PLFaLean

My journey of learning Lean 4 by implementing proofs from the wonderful book Programming Language Foundations in Agda.

Table of Contents

Volume 2

• 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

Volume 3

• 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

Appendix

• 1. Substitution: Substitution in the untyped lambda calculus