lean-pl-tutorials/README.org at main

Files

Hermes Agent 6e2914b06e migrate all tutorials from Markdown to Org mode

Converted with pandoc 3.7 (markdown → org), all 17 files:
- README, references, 15 tutorial units
- Internal file links updated from .md to .org
- Source code blocks (#+begin_src lean) preserved
- Tables, math notation, links intact

For the Emacs workflow.

2026-05-28 20:15:38 +02:00

2.0 KiB

Raw Permalink Blame History

Lean 4 + Programming Language Semantics

Lean 4 + Programming Language Semantics

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

├── 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

How to Use

Install Lean 4 (VS Code + lean4 extension): lean-lang.org/lean4/doc/quickstart.html
Start with Tutorial 1, Unit 1. Each unit is a standalone .org file with inline Lean exercises.
Type the exercises into a .lean file and make it compile.
After Tutorial 1, move to Tutorial 2 to mechanize STLC and HM.

Prerequisites

Functional programming (Haskell/OCaml familiarity)
Basic PL theory (lambda calculus, operational semantics, type systems)
No prior proof assistant experience required

References

See references.org for the full list of resources.