Local reasoning about programs that combine aliasing and mutable state remains a longstanding challenge in programming languages. Existing approaches—including ownership systems, linear and affine types, uniqueness types, and lexical effect tracking – enforce global restrictions such as uniqueness or linearity, or rely on shallow, syntactic analyses of captured variables. These designs limit expressive and pervasive reasoning, particularly in the presence of higher-order functions and shared mutable state. Reachability Types (RT) are a qualified type system for tracking aliasing and separation in higher-order programs, enabling runtime safety and non-interference guarantees. But current RT systems impose certain limitations, especially on its reference typing, in three key ways. First, they prohibit cyclic references, preventing the encoding of non-terminating computations and fixed-point combinators. Second, they enforce deep reference tracking, where a reference’s qualifier must include all transitively reachable locations, thus limiting reachability precision and interfering with optimizations such as fine-grained parallelism. Third, referent qualifier invariance prevents referents from escaping their allocation contexts, making patterns like reference factories inexpressible.

In this work, we address these limitations by extending RT with three mechanisms that enhance expressiveness. First, we introduce cyclic references, enabling recursive patterns to be encoded directly through the store. Second, we adopt shallow qualifier tracking, decoupling references from their transitively reachable values. Finally, we introduce an escaping rule with reference subtyping mechanism, allowing referent qualifiers to outlive their allocation context. These extensions are formalized in the $\lambda_{<:}^{\circ}$-calculus, along with a mechanized proof of type soundness via progress and preservation. We implement case studies to illustrate the expressiveness of the system through fixpoint combinators, non-interfering parallelism, and escaping, read-only references.