This appendix gathers the rule sheets used throughout the book. Each chapter’s section records the syntax and the full premises needed to reconstruct its derivations. Chapters that introduce no new primitive rules say so explicitly rather than presenting an empty table.
The foundational sheet below has no typing context and displays every premise it uses. Beginning with the dependent rule sheets, this appendix also makes presuppositions explicit: each such rule is a schema in a well-formed context with fresh bound variables, and the congruence scheme of subappendix A.4 applies to its term formers.
Sections Foundational judgments and untyped operational semantics Simple types, propositional proofs, and dynamics Intuitionistic first-order natural deduction and LJ Hindley–Milner polymorphism and the value restriction Semi-unification and polymorphic recursion Dimension types and units of measure Strict data rows and qualified row inference Type-preserving compilation of polymorphic records System F Higher-kinded polymorphism and existential packages Qualified types and dictionary evidence Generative ML modules, matching, and sharing MixML linking and definedness Modular type classes and implicit evidence Immutable-record subtyping and bounded quantification Polar algebraic subtyping and biunification Finite-graph Boolean semantic subtyping Top-free disjoint intersections and merge elaboration Difference refinements and source proof-carrying code Gradual source and ground-cast target Recursive types, PCF, domains, and finite observations Functional objects and recursive object representations Corrected simple-object row inference Positive Self, F-bounds, matching, and state Operation trees, CBPV, and deep handlers Scoped signatures and explicit substitution Higher-order signatures and modular elaboration Duplicate-label effect rows and inferred handlers Effect capabilities, explicit labels, and tunnelling Modal effects and the two source cards Lexical handlers, stack switching, and clue search Control calculi and dependent projection Linear and affine term calculus Structural rules The intensional base formers Extensional type theory: the delta HoTT additions Set truncation in T_hott TT^obs CCHM cubical type theory Cartesian cubical delta Cartesian cubical core Bunched implications and resource semantics Finite heaps and local Hoare logic Concurrent separation logic and Iris Ownership, borrowing, and affine protocols Swiftlet access discipline Region and capability interfaces Capture, typestate, and coeffect interfaces Graded bases, temporal typing, and soft logic Evaluation-strategy source and target calculi The unit-free ordered Lambek calculus Polarized propositional intuitionistic focusing Unit-free multiplicative proof nets First-order interaction nets GAL sharing graphs and the parallel-beta cost signature Computational type theory, elaboration, and clause compilation Uniqueness graphs and place calculi Pure type systems Logical frameworks and representations of binding Typed potentials and session protocols Names, HOL, and finite-type interpretation Selection products and restricted bar recursion Abstract interpretation and checked invariants Symbolic execution and information-flow rules Indexed signatures, records, and descriptions Accessibility, Mendler iteration, and guarded observations Interaction trees and compositional linearizability Logic enrichment, same-subject types, and erased induction Modular, linear, quantitative, and graded dependent systems Erasure, dependent protocols, effects, specifications, and partiality Dependent subtyping, object paths, and classical control Proof production, metaprogramming, levels, and generated actions Declaration processing, copatterns, and erasure Specialization, supercompilation, and staging