Immutable records and bounded quantification

The immutable call-by-value calculus contains $\mathsf{Top}$, $\mathsf{Bot}$, Unit, Booleans, naturals, arrows, products, sums, and finite-map records. Subtyping has reflexivity, transitivity, top, bottom, contravariant arrow domains, covariant products and sums, and width/depth record comparison. Subsumption is static and has no runtime coercion form.

Shape inversion through subsumption gives preservation, progress, and safety in theorem 8.10, theorem 8.11, corollary 8.12. The closed finite grammar has computable joins and meets by theorem 18.18. Record depth relies on immutability; no mutable-field theorem is claimed.

Kernel adds ordered type bounds, bounded type abstraction/application, source-variable promotion, and invariant comparison of universal bounds. Weakening, narrowing, type substitution, and term substitution are the strengthened package of theorem 8.18; the bounded extension is safe by corollary 8.21. The source-promoting priority algorithm terminates and is sound and complete by theorem 8.23, theorem 8.26. This decides supplied subtype queries; the chapter explicitly does not claim a complete bidirectional term checker, row inference, or principal types.

Full retains only variables, arrows, bounded universals, and top, and replaces the invariant Kernel rule by contravariant bound comparison with the body checked under the target bound. It does not inherit records, bottom, products, sums, or the Kernel decision algorithm. A statement may be closed relative to a nonempty well-formed bound context as fixed in definition 8.28.

The exact imported two-counter-to-rowing-to-subtyping reduction is theorem 8.29. The growing-context trace is only a mechanism example. The annotated application reduction gives undecidable typechecking under supplied bound contexts; see corollary 8.30. No executable artifact is used as evidence for either negative result.