Arrows go from each prerequisite to the units that depend on it. Hover or focus a unit to highlight its path.
- Mathematical induction article
- Inductive definitions and structural induction article
- Formal syntax and metavariables article
- Big-step operational semantics article
- Denotational semantics article
- First-order terms and unification article
- Product and sum types article
- Recursive types and algebraic data types article
- Bindings, free variables and alpha-equivalence article
- Capture-avoiding substitution article
- Simply typed lambda calculus article
- The substitution lemma for typing article