This appendix collects signatures and metatheorems in one place. Each block names an exact signature, its equality or conversion judgments, and the theorem boundary proved or imported in the owning chapter. Full-premise rules remain in appendix A .
Sections Rules, derivations, and untyped operational semantics Shared signatures Fields recorded External extension tracking Simply typed lambda calculus and intuitionistic propositions Intuitionistic first-order proof theory Hindley–Milner polymorphism and principal inference Semi-unification and Milner–Mycroft inference Dimension types and units of measure Strict data rows, qualified inference, and evidence Type-preserving compilation of polymorphic records System F Relational parametricity for System F Higher kinds, packages, and self-representation Qualified types and coherent dictionary elaboration Generative ML modules, sharing, and matching MixML, LTG, and definedness Modular type classes and implicit modules Immutable records and bounded quantification Algebraic subtyping and principal inference Finite-graph Boolean semantic subtyping Top-free disjoint intersections Difference-refinement array calculus Gradual source and ground-cast calculus Recursive types, domains, and general recursion Functional objects, recursive self, and representation Corrected inference for simple objects Positive Self, F-bounds, matching, and state Operation trees, CBPV, and deep handlers Scoped operations and explicit substitution Higher-order algebraic effects and modular elaboration Effect rows, inference, and handlers Effect-capability signatures, translations, and metatheorems Modal-effect signatures and preservation ledger Lexical-handler compilation ledger Control operators, CPS, and classical proofs Linear and affine term calculus Current migration status Bunched implications and resource semantics Finite separation logic Concurrent separation logic and Iris metatheory Ownership, borrowing, and affine protocols Swiftlet mutable values Region inference and capability memory management Capture, typestate, and coeffect signatures Graded bases, Simply RaTT, and SLL2 signatures Function-only evaluation-strategy translations Unit-free ordered Lambek calculus Polarized propositional intuitionistic focusing Unit-free multiplicative proof nets First-order interaction nets Optimal sharing, readback, and cost T_0 and its normalized subfragment Extensional, homotopical, and computed equality deltas Checked extension edges Computational meanings and untrusted Timpl front ends Checked front-end edges Uniqueness and ownership signatures Pure type systems and the lambda cube Encodings and binding theorem boundaries AARA and protocol theorem boundaries Nominal, HOL, and Dialectica theorem boundaries Bar-recursive choice theorem boundary Abstract-interpretation theorem boundaries Symbolic-execution and noninterference boundaries Dependent-core and Dybjer-source boundaries Universe presentation and paradox boundaries Identity, indexed-family, record, and description boundaries Container, recursion, termination, and coinduction boundaries Recursive-effect and concurrent-object boundaries Logic enrichment and erased dependent cores Rewriting and resource-sensitive dependency Erasure, dependent protocols, effects, specifications, and partiality Dependent subtyping, object paths, and classical control Kernel checking and definition processing Declaration checking, copattern compilation, and erasure Specialization, staging, and dependent generated code