Arrows go from each prerequisite to the units that depend on it. Hover or focus a unit to highlight its path.
- Formal syntax and metavariables article
- Scope and local state article
- Bindings, free variables and alpha-equivalence article
- Higher-order functions and function composition article
- Untyped lambda calculus article
- Simply typed lambda calculus article
- Capture-avoiding substitution article
- The substitution lemma for typing article
- Beta reduction and normal forms article