will post a preprint soon, but this paper explores the semantics of mutable references and specifically how type universes can describe regions of allocations. this allows us to describe stratified higher-order references, and prove termination of a language with higher-order references, as well as further distinguish between cyclic and acyclic full-ground references.