/plfa-but-Lean4

Learn Lean 4 with PLFA proofs.

Primary LanguageLeanMIT LicenseMIT

plfl

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