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
- Higher-order functions and function composition article
- Untyped lambda calculus article
- Beta reduction and normal forms article
- Evaluation strategies article
- Typing judgments and static semantics article
- Simply typed lambda calculus article
- Parametric polymorphism article
- Curry-Howard correspondence article
- The substitution lemma for typing article