This appendix records recurring notation, its semantic role, and its first substantive use. The first-occurrence column names the chapter in which a symbol becomes part of the working language; an earlier informal mention does not establish its binding or scope. It is a reverse index rather than a teaching sequence. The Chapter 1 entries are collected in subappendix C.5 ; every other row names the later chapter that defines its objects.
Sections Global metalanguage Reverse glyph index Judgments and contexts Hindley–Milner inference Foundational derivations, programs, and proofs First-order proofs Semi-unification and polymorphic recursion Dimensions and units of measure Strict data rows Polymorphic record compilation System F Relational parametricity Higher kinds, packages, and elaboration Qualified types, evidence, and ML modules MixML linking and definedness Modular type classes and implicit evidence Immutable records and bounded subtyping Algebraic subtyping and biunification Semantic subtyping Disjoint intersections and merge elaboration Difference refinements and certificates Gradual types and casts Recursive types, domains, and observations Functional objects and recursive self Corrected simple-object inference Self types, F-bounds, and matching Effects, CBPV, and algebraic handlers Scoped operations and explicit substitution Higher-order signatures and modular elaboration Effect rows and principal handler inference Effect-capability and tunnelling notation Modal-effect and encoding notation Lexical handlers and direct compilation Control operators and classical proofs Linear and affine types Explicit substitutions Type formers and terms Pure type systems Frameworks, names, and contextual objects Universes Homotopy type theory Cubical type theory Observational type theory Categories and categories with families Dependent and computed-equality distinctions General notation Bunched implications and resource semantics Separation logic Concurrent separation logic and Iris notation Ownership and borrowing Mutable value access Regions and capabilities Capture, typestate, and coeffect notation Graded-base, temporal, and soft-logic notation Evaluation-strategy translations Ordered Lambek calculus Polarization and focusing Proof nets and switchings Interaction nets Optimal sharing and graph reduction Uniqueness graphs and places Resource and protocol notation Selection products and bar recursion Abstract domains, paths, and machine abstraction Symbolic paths and security observations Identity, records, and datatype descriptions Containers, descent, Mendler iteration, and observations Logic-enriched and erased same-subject notation Interaction trees, modules, and possibilities Rewriting, shape, quantity, and graded modality Graded extraction and partial computations Dependent boundaries, stable paths, and controlled dependencies Kernel and normalization semantics Proof production, levels, casts, and generated action Declaration processing Specialization, driving, and staged terms