* Lean 4 + Programming Language Semantics
:PROPERTIES:
:CUSTOM_ID: lean-4-programming-language-semantics
:END:
A self-study curriculum for computer scientists who know PL theory and want
to mechanize proofs in Lean 4 --- from syntax to soundness of the
Hindley-Milner type system.

** Structure
:PROPERTIES:
:CUSTOM_ID: structure
:END:
#+begin_example
├── README.org                          ← this file
├── tutorial-01-basics/                ← Lean 4 fundamentals
│   ├── 01-types-and-functions.org
│   ├── 02-inductive-types.org
│   ├── 03-propositions-and-proofs.org
│   ├── 04-quantifiers-and-equality.org
│   ├── 05-advanced-tactics.org
│   ├── 06-structures-type-classes.org
│   └── 07-dependent-types.org
├── tutorial-02-semantics/             ← PL semantics in Lean
│   ├── 08-syntax-representation.org
│   ├── 09-substitution.org
│   ├── 10-small-step-semantics.org
│   ├── 11-stlc-type-system.org
│   ├── 12-type-safety.org
│   ├── 13-hm-declarative.org
│   ├── 14-algorithm-w.org
│   └── 15-soundness-completeness.org
└── references.org                      ← all cited resources
#+end_example

** How to Use
:PROPERTIES:
:CUSTOM_ID: how-to-use
:END:
1. Install Lean 4 (VS Code + =lean4= extension):
   [[https://lean-lang.org/lean4/doc/quickstart.html][lean-lang.org/lean4/doc/quickstart.html]]
2. Start with *Tutorial 1*, Unit 1. Each unit is a standalone =.org= file with
   inline Lean exercises.
3. Type the exercises into a =.lean= file and make it compile.
4. After Tutorial 1, move to *Tutorial 2* to mechanize STLC and HM.

** Prerequisites
:PROPERTIES:
:CUSTOM_ID: prerequisites
:END:
- Functional programming (Haskell/OCaml familiarity)
- Basic PL theory (lambda calculus, operational semantics, type systems)
- No prior proof assistant experience required

** References
:PROPERTIES:
:CUSTOM_ID: references
:END:
See [[file:references.org]] for the full list of resources.