appendix sectionsignatures

Capture, typestate, and coeffect signatures

${CF}_{<:}$ capture tracking

Signature.: The core is the paper’s call-by-value System $F_{<:}$ extension with finite or universal capture sets, capture-annotated pretypes, capture-dependent arrows, polarity-indexed formation, subcapturing, subtyping, and simultaneous term/capture substitution at beta.
Results.: Covariant capture substitution and value substitution are lemma 51.4, lemma 51.6. Preservation, progress, and prediction are theorem 51.7, theorem 51.8. The archived paper-era Coq development owns the complete infrastructure and all ordinary $F_{<:}$ cases.
Extension boundary.: The escape condition belongs to the source’s separate capability extensions. It uses core prediction only after adding delimiter syntax and typing. Scala documentation is surface evidence.
Separate boxed card.: The pure/captured grammar, explicit box and unbox forms, monadic-normal-form machine, and state typing of ${CC}_{<:}^{◻}$ own the preservation and progress result in theorem 51.9. No result transfers between that signature and the preceding unboxed ${CF}_{<:}$ card.
Not claimed.: Capture sets are not effects, lifetimes, ownership quantities, or confinement proofs. The selected source states no closure-conversion theorem, and the finite Kappa checker proves no metatheorem.

Signature.: The book-owned kernel has three file states, four protocol edges, affine state-indexed handles, flow-sensitive administrative programs, a common-output branch rule, recursive checked procedures, and a finite heap with injective handle agreement. A procedure signature uses $⊸$ because its codomain is a protocol context, not a type; procedure-local handles cannot escape its first-order result context.
Results.: One-step state preservation is lemma 52.2; protocol progress and safety are lemma 52.3, theorem 52.4. The proof covers every rule of this finite kernel.
Source boundary.: Strom–Yemini, modular typestate, and Featherweight Typestate retain their own analyses, permissions, object languages, and theorems. No translation into or out of the book kernel is claimed.
Not claimed.: Safety excludes unavailable operations. It establishes neither termination, eventual close, communication fidelity, deadlock freedom, nor temporal liveness.

Flat call-by-value.: The scalar has sequential and sharing monoids, two-sided distributivity, a preorder, and flat combination satisfying condition $F$ . Pure-value substitution and subject reduction are lemma 53.1, theorem 53.2.
Flat call-by-name.: The same flat syntax supports subject reduction only under the top-pointed or bottom-pointed hypotheses stated in lemma 53.3, lemma 53.4, theorem 53.5. No result transfers from one case merely because both annotations are flat.
Structural.: Per-variable vectors, vector-respecting structural rules, the locally sound and complete context-transformation package, and the scalar axioms give structural substitution and subject reduction in lemma 53.6, theorem 53.7. The relation in this theorem is unrestricted compatible beta reduction. The unique bound-variable position is the decisive difference from flat substitution.
Models and boundary.: The chapter proves elementwise dictionary and finite-power calculations for implicit parameters and bounded reuse. Its dataflow fragment has only the dedicated lookup bound. No complete dataflow metatheory, cache optimality, graded-modality correspondence, or combined effect–coeffect theorem is claimed. The Kappa artifact implements finite analyses only.