plfl

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

Table of Contents

Volume 2

• [x] 1. Lambda: Introduction to Lambda Calculus
• [x] 2. Properties: Progress and Preservation
• [x] 3. DeBruijn: Intrinsically-typed de Bruijn representation
• [x] 4. More: Additional constructs of simply-typed lambda calculus
• [x] 5. Bisimulation: Relating reduction systems
• [x] 6. Inference: Bidirectional type inference
• [x] 7. Untyped: Untyped lambda calculus with full normalisation
• [x] 8. Confluence: Confluence of untyped lambda calculus
• [x] 9. BigStep: Big-step semantics of untyped lambda calculus

Volume 3

• [x] 1. Denotational: Denotational semantics of untyped lambda calculus
• [x] 2. Compositional: The denotational semantics is compositional
• [x] 3. Soundness: Soundness of reduction with respect to denotational semantics
• [x] 4. Adequacy: Adequacy of denotational semantics with respect to operational semantics
• [x] 5. ContextualEquivalence: Denotational equality implies contextual equivalence

Appendix

• [x] 1. Substitution: Substitution in the untyped lambda calculus