Region inference and capability memory management

The Tofte–Talpin judgment annotates a skeletal ML term with placed types, region operations, and read/write effects. Milner refinement is theorem 50.1; semantic correspondence is theorem 50.2 at the source’s consistency relation.

Memory is partitioned into named regions and typing carries unique or duplicable region authority. Preservation/progress, memory safety, and complete collection are theorem 50.5, corollary 50.6, theorem 50.7.

The technical report’s CPS translation maps annotated region effects to capabilities. Its exact closed type-preservation result is theorem 50.8; unannotated inference remains owned by the separate Tofte–Talpin spine.

Cyclone, L${}^3$, linear regions, and monadic regions retain distinct signatures and source theorems (definition 50.9, definition 50.11, definition 50.13). The linear-regions encodings are sketches into a target with proved safety, not separately stated translation theorems. No theorem transfers merely because all four systems mention regions or locations.

The chapter proves typed memory safety, not object-capability confinement, ambient-authority security, race freedom, allocator correctness, or correspondence between a historical compiler and a formal core. Appendix E’s Kappa program is only a finite trace auditor.