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
- Judgments and inference rules article
- Small-step operational semantics article
- Evaluation contexts article
- Continuations and continuation-passing style article
- Observational equivalence article
- Semantics-preserving program transformations article
- Mathematical statements and quantifiers article
- Symbolic execution and path conditions article
- The substitution lemma for typing article
- Type safety through progress and preservation article