Arrows go from each prerequisite to the units that depend on it. Hover or focus a unit to highlight its path.
- Bindings, free variables and alpha-equivalence article
- Capture-avoiding substitution article
- Untyped lambda calculus article
- Beta reduction and normal forms article
- Evaluation strategies article
- Simply typed lambda calculus article
- Inductive definitions and structural induction article
- The substitution lemma for typing article
- Type safety through progress and preservation article