Hermes Agent
6e2914b06e
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.
59 lines
2.0 KiB
Org Mode
59 lines
2.0 KiB
Org Mode
* 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.
|