Arrows go from each prerequisite to the units that depend on it. Hover or focus a unit to highlight its path.
- Inductive definitions and structural induction article
- Formal syntax and metavariables article
- First-order terms and unification article
- Logic programming with facts, rules and queries article
- Judgments and inference rules article
- Fixed points of functions article
- Denotational semantics article
- Big-step operational semantics article
- Scope and local state article
- Environments and stores in language semantics article
- Bindings, free variables and alpha-equivalence article
- Capture-avoiding substitution article
- Untyped lambda calculus article