Paper Content:
Page 1:
Complete the Cycle: Reachability Types with Expressive
Cyclic References
HAOTIAN DENG, Purdue University, USA
SIYUAN HE, Purdue University, USA
SONGLIN JIA, Purdue University, USA
YUYAN BAO, Augusta University, USA
TIARK ROMPF, Purdue University, USA
Reachability Types (RT) are a qualified type system for tracking aliasing and separation in functional and
higher-order programming. By formalizing resource reachability with a sound static type system, RT enable
higher-order programming patterns with runtime safety and non-interference guarantees. However, previous
RT systems have been based on calculi that restrict cyclic dependencies and are shown to be terminating
in the absence of built-in recursive constructs. While termination is sometimes a desirable property, sim-
plifying reasoning and ensuring predictable behavior, it implies an inability to encode expressive programs
involving non-termination and advanced recursive patterns, such as mutual recursion and various fixed-point
combinators.
In this paper, we address this limitation by extending RT with an expressive cyclic reference type that
permits the formation of cyclic dependencies through the store, thereby allowing the system to encode
recursive programming patterns without relying on extra built-in constructs. In addition, we redesign qualifier
typing in the reference introduction rule, allowing separate references to point to a shared and tracked referent.
We formalize the system as the 𝜆◦<:-calculus, with a mechanized soundness proof via the standard progress
and preservation lemmas. As a demonstration, we implement a well-typed fixpoint operator, proving that
recursive patterns can be encoded using the novel cyclic reference type.
CCS Concepts: •Software and its engineering →Semantics ;Functional languages ;General program-
ming languages .
1 Introduction
The challenge of bringing local reasoning to sharing and aliasing has been thoroughly explored in
the development of ownership systems [Clarke et al .2013, 2001, 1998; Hogg 1991], linear/affine
types [Girard 1987; Wadler 1990], and uniqueness types [Barendsen and Smetsers 1996]. These ideas
have also seen practical adoption: notably, Rust [Matsakis and II 2014] incorporates concepts from
both uniqueness types and ownership systems to provide strong static memory safety guarantees
in a low-level systems language; Linear Haskell [Bernardy et al .2018] extends Haskell’s type
system with linear types, controlling the multiplicity of resource use; Scala Capture Types [Boruch-
Gruszecki et al .2023] introduce capturing sets to track free variables in a value, preventing illegal
captures and escapes.
Inspired by separation logic [Reynolds 2002], Reachability Types (RT) [Bao et al .2021; Wei et al .
2024] are a recent proposal to bring reasoning about memory sharing and separation to higher-level
functional languages. While Rust, a systems-level language, enforces safety through global heap
invariants—specifically, the “shared XOR mutable” uniqueness constraint—Linear Haskell and Scala
Capture Types, as higher-level languages with garbage collection, focus on specific usage patterns,
such as linearity or particular resource types like captured effects. In contrast, RT provides a more
Authors’ Contact Information: Haotian Deng, Purdue University, West Lafayette, IN, USA, deng254@purdue.edu; Siyuan
He, Purdue University, West Lafayette, IN, USA, he662@purdue.edu; Songlin Jia, Purdue University, West Lafayette, IN,
USA, jia137@purdue.edu; Yuyan Bao, Augusta University, USA, yubao@augusta.edu; Tiark Rompf, Purdue University, USA,
tiark@purdue.edu.arXiv:2503.07328v1 [cs.PL] 10 Mar 2025
Page 2:
2 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
1valc : Ref[(Unit => Unit)q]c
2deff(x : Unit) = {(!c)(x)}
3//⊣[ f : (Unit => Unit)c]
4c := f // error! c ≮:q
5// (Unit => Unit)c≮:(Unit => Unit)q
(a) Landin’s knot is not typeable in 𝜆q([Wei et al .
2024]) due to the lack of cyclic references. Line 4
fails to type check because the referent qualifier
qcan only reach observable resources before cis
declared, which does not include c.1valc :𝝁𝑧.Ref[(Unit => Unit)z]c
2deff(x : Unit) = {(!c)(x)}
3//⊣[ f : (Unit => Unit)c]
4c := f
5// Okay, because c is a cyclic reference
(b) Landin’s knot typed with a cyclic reference in
𝜆◦<:(this work). Line 4 is type checked with
t-sassgn-v . Its reachability graph is shown below
(Figure 1c).
c:𝜇z.Ref[(Unit => Unit)𝑧]𝑐f =𝜆x.(...c...):(Unit => Unit)𝑐c := f
f : (Unit => Unit)c
(c) Reachability graph of a well-typed cyclic reference assigned with a self-capturing function,
expressing a simple cycle through the store (this work).
Fig. 1. Typing Landin’s Knot
flexible alternative, enabling selective enforcement of uniqueness, linear usage, resource capturing,
and other patterns through reachability tracking and a flow-sensitive effect system [Bao et al .2021].
However, RT’s treatment of reference typing has limited expressiveness and flexibility due to (1)
a lack of cyclic references and (2) constrained, imprecise reference qualifiers.
1.1 Lack of Cyclic References
Recent theoretical advances in RT have shown that variants of RT that support higher-order
references remain terminating [Bao et al .2023]. This is counterintuitive, as higher-order state
typically permits cycles in the store, thereby enabling unrestricted general recursion.
In fact, it turns out that RT prohibit creating such cycles through the store, due to the absence of
cyclic reference types. As shown in Figure 1a, Landin’s Knot, an idiomatic way to construct cyclic
dependencies through higher-order state, is not typeable in Wei et al .[2024]’s polymorphic 𝜆q
system due to its restriction on cyclic references.
We address this limitation by first providing a brief overview of RT (Section 2.1), presenting
potential challenges of supporting cyclic reference typing with RT, and then explaining our approach
to overcome these challenges (Section 2.2). We further demonstrate how our solution enables the
correct typing of Landin’s Knot in Section 2.3 by supporting cyclic references.
1.2 Constrained, Imprecise Reference Qualifiers
Wei et al .[2024]’s reference typing employs a "deep" tracking mechanism, which tracks not only the
reference itself but also its transitively reachable locations. While this approach ensures soundness,
it constrains the heap structures expressible with nested references and introduces imprecision in
reference tracking.
Page 3:
Complete the Cycle: Reachability Types with Expressive Cyclic References 3
𝜆
T⊥
Ref[T⊥]Ref[T⊥](a) Reachability graph of Bao et al .[2021]’s system. Be-
cause references are first-order with untracked referents
(depicted as a dotted gray cloud), the system cannot rep-
resent hierarchical structures using reference types.
Ref[Tp]qRef[Tq]q...𝜆...𝜆...
...... ...
(b) Reachability graph illustrating the “deep sep-
aration” reference tracking model in Wei et al .
[2024]’s system. References marked with qare
separate from each other and enforce strict sepa-
ration of all transitively reachable locations. Un-
tracked data, which separate references may still
reach, is depicted as dotted gray clouds.Ref[Tp]qRef[Tq]q...𝜆...𝜆
𝜆...
... ...
(c) Reachability graph illustrating the "shallow
separation" reference tracking model in 𝜆◦<:(this
work). Unlike Wei et al .[2024]’s system, our model
allows separate references to share child nodes (de-
picted in yellow ). Additionally, the system sup-
ports cyclic references where values can reach the
references themselves (highlighted in purple ).
Fig. 2. Reachability graph illustrating references in Bao et al .[2021], Wei et al .[2024], and this work. The
𝜆-labeled clouds represent non-location values, and the circular nodes ( ⃝) represent store locations. All
store locations are tracked (we denote tracked values using pale blue ). We discuss a concrete example
in Section 2.4.
As illustrated in Figure 2b, separate references1remain not only distinct themselves but also
strictly separate from each other in terms of their transitively reachable locations.2This restriction
prevents parent references from sharing store locations, further limiting the expressiveness of heap
structures involving nested references.
Beyond structural constraints, this overapproximation of reference reachability affects precision
in reference typing. For instance, extending the system with effect tracking to model a linked-list
structure would cause an update to a single node to affect the entire list, violating the intended
semantics. The inability to distinguish between a reference and its reachable locations limits
expressiveness in programs that require fine-grained reference tracking.
To address these limitations, we refine the reference introduction rule, allowing references to
share underlying objects while preserving soundness (Section 2.4).
1Separation is indicated by the qmarker, which signifies contextual freshness. Resources with a sole qmarker only reach
contextually fresh objects and are considered separate from currently observable resources. See Section 2.1 for a detailed
explanation of the qmarker.
2This follows directly from t-ref , whereqappears in the qualifiers of both the inner referent and the outer reference. As a
result, the outer qualifier always includes all transitively reachable locations.
Page 4:
4 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
This Work .In this work, we extend RT’s reference typing in two directions to improve the
expressiveness of the system.
First, we introduce well-typed cyclic references that store values which may capture the reference
itself. This is key to enabling recursive programming patterns within the primitive RT framework
without built-in recursion support, allowing the system to type-check various non-terminating
applications (Section 4). The presence of cycles introduces complexity not encountered in previous
systems. In particular, the assignment operation of cyclic references must be carefully controlled in
order to maintain the soundness of the type system (Section 2.2). We observe that by requiring
the assigned reference term to be a variable, and the assignee’s qualifier to be a singleton qualifier
matching that variable, we can effectively retain soundness in the presence of mutable references
containing cycles through the store (Section 3.2).
Second, we introduce shallow and precise reference tracking, allowing separate references to
contain shared objects indirectly. This design improves the precision of reference qualifiers by
distinguishing references from their transitively reachable locations. Consequently, this design
also enables the construction of graph structures in the reachability hierarchy not possible in prior
systems (cf. Figure 2c).
We present the 𝜆◦
<:-calculus, which enables the typing of cyclic references in the presence of
reachability tracking. Specifically, it enables the language to express advanced non-terminating
patterns through a fixed-point operator (see Section 4).
Contributions and Organization .The main contributions of this paper are as follows:
•We informally present the encoding of recursion using cyclic references alone in RT, without
relying on built-in language support (Section 2). We present basic concepts of RT (Section 2.1),
key ideas of this work including cyclic references (Section 2.2) leading to the typing of
Landin’s Knot in RT (Section 2.3), and precise reference tracking (Section 2.4).
•We present the 𝜆◦
<:-calculus, a variant of the RT systems that permits well-typed cyclic
structures with a cyclic reference type (Section 3), covering basic syntax (Section 3.1), static
typing (Section 3.2), dynamic typing (Section 3.3), implementation details of the mechanized
proof (Section 3.4), as well as meta-theory (Section 3.5) leading to the main soundness result.
•We present a case study on a fixed-point combinator that demonstrates 𝜆◦
<:’s ability to write
non-terminating programs (Section 4).
We discuss related work in Section 5, and in Section 6, we address limitations of this work as
well as the trade-offs that justify our design decisions. As in Wei et al .[2024], we extend the system
with type polymorphism in the style of system F <:and fully mechanize it in Coq, showing type
soundness by proving the progress and preservation lemma.3
2 Reachability Types (RT)
In this section, we introduce key concepts of Reachability Types (RT) (Section 2.1), discuss cyclic
references (Section 2.2) and their role in typing examples such as Landin’s Knot (Section 2.3), and
explore shallow reference tracking (Section 2.4).
2.1 Key Ideas of RT
Type Qualifiers: Tracking Named, Reachable Resources .Reachability Types assign type
qualifiers to terms, in addition to types. The type qualifiers keep track of the reachable set of resource
of a given term, thus providing static guarantee about resource sharing and separation.
3The proof artifact can be found at https://github.com/TiarkRompf/reachability.
Page 5:
Complete the Cycle: Reachability Types with Expressive Cyclic References 5
Type qualifiers are finite sets of names used in the program, optionally including the qmarker
that signifies a fresh resource (See Figure 4). For example, a variable (that is a reference to an
(untracked) integer value) named counter naturally tracks itself with its qualifier, and has counter in
its own qualifier signifying this tracking:
valcounter = newRef(0) // : Ref[Int]counter⊣[ counter: Ref[Int]...]
When an alias is created for the counter variable, the alias has counter in its qualifier:
valcounter2 = counter // : Ref[Int]counter2⊣[ counter2: Ref[Int]counter
, counter: ... ]
Note that through the context, we can trace the reachability of resource.
For functions, qualifiers keep track of their captured variables . For example, in an idiomatic,
functional implementation of the counter increment method inccaptures the free variable counter ,
and this capturing is reflected in its observability qualifier:
def inc(n: Int): Unit = { counter := !counter + n } // : inc: (Int => Unit)counter
In addition to the qualifier, function argument type and return type also have their qualifiers. We
refer readers to Wei et al .[2024] for a complete description at the meaning of function argument
qualifier and return qualifier.
Fresh Marker q: Tracking Unbound, Freshly Allocated Resource .Qualifiers can also be a
special marker (a.k.a. the “fresh” marker, denoted by the qsymbol), which serves a dual purpose
depending on their occuring context. We illustrate the two purposes below.
1. Fresh Marker in Regular Qualifier. When qoccurs in the qualifier of a concrete resource, it
signifies that the resource is a freshly allocated resource that is not (yet) bound to a name. For
example, a newly created reference has a qas its type qualifier:
newRef(0) // : Ref[Int]q
As the fresh resource is bound to a variable name, the context keeps track of the fact that the
name refers to a fresh resource, and the fresh marker no longer appears in the variable:
varcounter = newRef(0) // : Ref[Int]counter⊣[ counter: Ref[Int]q]
2. Fresh Marker in Function Argument Qualifier. Whenqappears in a function argument qualifier,
it signifies that the argument may contain unobservable resources, allowing the function to be used
in a growing application (a.k.a. a “fresh” application). This means that the function does not assume
a fixed set of reachable variables in its argument but instead allows qualifiers that can expand
during evaluation.
A key motivation for using qin function arguments is to prevent incorrect aliasing assumptions.
Specifically, function applications must enforce a separation constraint between the function’s
qualifier and the argument’s qualifier. If the function were allowed to access an argument with an
overlapping qualifier, inconsistencies in qualifier tracking could arise.
Consider the following identity function, which simply returns its argument:
defid(x: Tq): Tx= x
Here, the argument xis marked with q, meaning that the function does not assume any aliasing
relationships between xand the function’s environment. This allows idto be applied to newly
allocated or untracked resources without interfering with existing references. However, failing to
enforce this separation constraint can lead to unsound aliasing. Consider the following function,
which modifies its argument:
defupdate(x: Ref[Int]q): Unit = {
counter := !(x) + 1
}
Applying update to an argument that aliases counter violates the separation constraint:
Page 6:
6 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
update(counter) // Invalid: counter overlaps with x
The issue arises because counter is a tracked resource that already appears in the function’s
environment, whereas xis marked with q, indicating that it should be fresh or previously untracked.
The function body assumes that xis disjoint from its environment, but in this case, xaliases
counter , leading to a violation. By enforcing the separation constraint with q, we prevent function
applications where the argument is already part of the function’s tracked environment. This ensures
that function bodies do not inadvertently mix fresh and existing references, preserving sound alias
tracking.
Again, we refer readers to Wei et al .[2024] for details (See t-app-fresh for the formal typing
rule of fresh applications).
Reference Type: Mutable Cells .So far, the examples involving reference types only have base
types ( e.g.Int) as the referent type, whose qualifier is untracked ( ∅), and thus elided. In fact, Wei
et al.[2024]’s system does support references with referent qualifiers, and the assigned referent
must possess only the specified qualifier:
vala = ... // : Ta
valb = ... // : Tb
valcell = newRef(...) // : Ref[Ta
]...
cell := a // Okay
cell := b // Error: referent qualifier mismatch!
As shown above, since cellhasaas its referent qualifier, it is only permitted to assign cellwith
a(or any resource whose qualifier is upper-bounded by a), and an attempt to assign it with, for
example, b, will trigger a type error.
Qualifier Subtyping: Subset Relation .Qualifiers in RT support subtyping, following an intu-
itive subset relation where a qualifier can be upcast to a “larger” qualifier (See q-sub ).
For example, in the code below, the qualifier of the reference cellis adjusted to allow both aand
bwith qualifier subtyping:
vala = ... // : Ta
valb = ... // : Tb
valcell = newRef(...) // : Ref[Ta,b
]...
cell := a // Okay. Ta
<: Ta,b
cell := b // Okay. Tb
<: Ta,b
Here, subtyping allows precise tracking of aliasing relationships: since TaandTbare both subtypes
ofTa,b, the reference cell can safely store either.
Additional qualifier subtyping rules are presented in Figure 6, and we refer readers to Wei et al .
[2024] for an in-depth discussion.
Limited Reference Typing .Building on Bao et al .[2021]’s system, which only supports un-
tracked, first-order references, Wei et al .[2024] extend reference typing to handle nested references.
However, their system imposes the following constraints:
(1)The referent qualifier must be in scope when the reference is created, prohibiting cyclic
references.
(2) The referent qualifier is always included in the qualifier of the newly created reference.
The first constraint prevents cyclic dependencies between the referent and the reference. Specifi-
cally, it disallows the referent qualifier from depending on the reference qualifier that contains it.
As a result, cyclic constructs such as Landin’s Knot cannot be typed (See Figure 1a). The second
constraint introduces an unnecessary coupling between the reference (parent node) and its referent
Page 7:
Complete the Cycle: Reachability Types with Expressive Cyclic References 7
First-Order
Reference
(Bao et al .[2021])4Nested
Reference
(Wei et al .[2024])5Non-Cyclic
Reference
(This work)Cyclic
Reference
(This work)
y = new
Ref(e)𝑦:Ref[𝑇⊥]𝑞
𝑒:𝑇⊥𝑦:Ref[𝑇𝑞]𝑞,q
𝑒:𝑇𝑞𝑦:𝝁𝑥.Ref[𝑇𝑞]q
𝑒:𝑇𝑞𝝁𝑥.Ref[𝑇𝑥,𝑞]q
𝑒:𝑇𝑞
y := x 𝑥:𝑇⊥𝑥:𝑇𝑞𝑥:𝑇𝑞𝑥:𝑇𝑞,𝑦
! y !𝑦:𝑇⊥!𝑦:𝑇𝑞!𝑦:𝑇𝑞!𝑦:𝑇𝑞,𝑦
Fig. 3. Comparison of Reference Typing Rules in RT.
(child node), limiting the ability to track separate references that share the same referent (See
Figure 2b).
To address constraint (1), we introduce a more expressive core language capable of typing cyclic
constructs such as Landin’s Knot and similar recursive programs (Section 2.2, Section 2.3). We
resolve constraint (2) by refining the reference typing mechanism, which we discuss in Section 2.4.
We list the key differences of reference types with other variants of RT systems in Figure 3.
2.2 Cyclic References
In order to address constraint (1), we introduce a more expressive reference type that allows
the inner referent qualifier to refer to its enclosing, outer reference qualifier. We denote the new
form of reference as 𝝁𝑧.Ref[𝑇𝑞]𝑝, where 𝝁𝑧creates a binder that can be included in the inner
referent qualifier 𝑞, to refer to the reference itself. This extension is key to enabling cyclic references
where the referent qualifier can capture its containing reference cell. The idea is that when the
bound variable 𝑧is present in the referent qualifier 𝑞, we permit updating the referent with values
containing a cyclic pointer to the reference itself through the reference assignment operator:
valouter = newRef(...) // 𝝁𝑧.Ref[Tz]outer
valinner = ... // Touter
outer := inner // Okay
This construct introduces a cyclic dependency: the variable inner reaches reference outer (as
indicated by its qualifier), while outer , being a cyclic reference, can containinner via the assignment
operator.
However, incorporating cyclic dependencies into the type system is non-trivial, as it must remain
sound in their presence. Consider a naive (and erroneous) assignment rule t-sassgn-err :6
Γ𝜑⊢𝑡1:𝝁𝑧.Ref[𝑇𝑧,𝑞]𝑝
Γ𝜑⊢𝑡2:𝑇𝑝,𝑞
Γ𝜑⊢𝑡1B𝑡2:Unit∅(t-sassgn-err)
The first premise requires that 𝑡1has a cyclic reference type, where its referent qualifier can
reach either 𝑞or itself (indicated by 𝑧). The second premise states that any term 𝑡2can be assigned
to𝑡1as long as its qualifier does not exceed 𝑞and the qualifier of 𝑡1, denoted by 𝑝.
4Bao et al .[2021] used⊥to denote untracked qualifiers, which is semantically equivalent to ∅in later systems. Their system
does not have an equivalent concept of “freshness”.
5In this system, it is possible for references to have the qqualifier alone under a different context through fresh application
(t-app-fresh ), but it is impossible to produce separate references that encapsulate a shared value (See Section 2.4).
6This rule also lacks an additional premise q∉𝑞, which is not discussed in this section. The design decisions around this
rule are explored further in Section 3.2.
Page 8:
8 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
While this rule provides flexibility for cyclic dependencies, it introduces a serious issue in the
presence of subtyping. Specifically, it permits an assignee with anyqualifier to be assigned to a
self-reference, which violates the intended semantics of cyclic references.
To see why this is problematic, consider the following example, where the qualifier of the self
reference e1is upcasted to (incorrectly) accommodate an arbitrary qualifier in e2, ande2is also
upcasted to include e1in its qualifier:
vale1 = newRef(...) // : 𝝁𝑥.Ref[Tx]e1
vale2 = ... // : Te2,a,b,c,d,e
e1 := e2 // Unsound operation permitted by t-sassgn-err!
// e1: 𝝁𝑥.Ref[Tx]e1<:𝝁𝑥.Ref[Tx]e1,e2,a,b,c,d,e
// e2: Te2,a,b,c,d,e<: Te1,e2,a,b,c,d,e
This operation is clearly unsound, yet it would be naively permitted by t-sassgn-err . This issue
arises because upcasting of a cyclic reference’s outer qualifier allows it to generalize beyond its
original scope. If assignments were based on the outer qualifier (as in t-sassgn-err ), the system’s
qualifier tracking would become inconsistent.
The key to fixing this issue is to constrain the assigned reference to a variable and the assignee’s
qualifier to a singleton qualifier (i.e.∈P 1, see Figure 4), as shown in t-sassgn-v . We discuss this
rule in detail in Section 3.2.3. Restricting assignment to variable terms and singleton qualifiers
ensures safety, because at runtime, a variable of reference type ( e.g.e1in this case) will always be
substituted into a single location, and the assignee’s singleton variable qualifier ( e.g.e2) will be
substituted into the exact same singleton location qualifier.
With the correct typing rule ( t-sassgn-v ) in place, the system would reject the assignment
operation thereby retaining soundness:
e1 := e2 // Error: e2’s qualifier must be exactly e1
// e2: Te2,a,b,c,d,e̸<: Te1
2.3 Landin’s Knot: Type Checked
We now take a closer look at how cyclic references can allow RT to type a prime example of cycle
through store: the Landin’s Knot. We explain the key components that enable such typing in the
presence of reachability tracking without sacrificing the overall soundness of the system.
Landin’s Knot [Landin 1964] is a lightweight method to encode recursion in a non-recursive
lambda calculus utilizing higher-order state. Below is a typical implementation of Landin’s Knot
(with Scala surface syntax):
valc;deff(x) = {(!c)(x)}; c := f
In the above example, cis a pointer to a reference cell in memory, and fis a function that invokes
itself through the memory cell c. The assignment operation c := f “ties” the knot by assigning c
with the desired function, after which, calling fwill initiate an infinite sequence of recursive calls
to function f. Now, we highlight two limitations of the existing RT systems that prevent the typing
of the Landin’s Knot.
One key challenge with the encoding of Landin’s Knot in the presence of reachability tracking
lies in the need to assign a self capturing referent into the reference itself. Note that in Figure 1a, we
cannot simply assign qualifier cto the referent type Unit => Unit because the referent qualifier
must already be in the current context prior to being used at the reference creation site, as demanded
by constraint (1) mentioned in Section 2.1.
However, equipped with cyclic references, Figure 1b shows how the use of a cyclic reference
with a carefully controlled assignment operation ( t-sassgn-v ) can delegate the inner qualifier to
the outer qualifier, thus correctly typing Landin’s Knot. Note that as mentioned in Section 2.2, the
Page 9:
Complete the Cycle: Reachability Types with Expressive Cyclic References 9
program only type checks because the assigned cyclic reference is of the variable form, whose
singleton qualifier is present in the assignee’s qualifier set. This is key to ensuring the soundness
of the system in the presence of cyclic structures, because it rules out illegal qualifier growth by
restricting the assignee’s qualifier to a singleton qualifier matching a fixed variable term form. The
typed Landin’s knot is illustrated in Figure 1c.
We discuss technical details regarding the typing rules on cyclic references in Section 3.
2.4 Shallow, Precise Reference Tracking
Constraint (2) stems from a design decision in Wei et al .[2024] that enforces a saturated, deep
dependency on the reference qualifiers, in the sense that the reference’s (outer) qualifier always
subsumes the referent’s (inner) qualifier. This design creates unnecessary coupling between the
inner and the outer qualifier, and leads to imprecise reachability tracking.
Consider a reference cellthat contains an inner element a, under Wei et al. [2024]’s system:
vala = ... // : Ta
valcell = newRef(a) // : (Ref[Ta])cell,a
// Imprecision! cell and a are separate, but treated as shared
cell’s qualifier overapproximates its reachable sets by including the qualifier of its enclosed
element a. While such treatment is safe, it is largely imprecise and precludes complex uses of
references where a more granular tracking precision is desired. Suppose we extend the system with
flow-sensitive use effects upon reference assignment, then reassigning cellwould also impose a
use effect on a, which is imprecise:
cell := ... // (cell, use) ⊲(a, use)
// a appears to be used, even though it is not used
Note that under Wei et al .[2024]’s system, it is possible to create a function ( e.g.newctx ) that
attempts to “remove” the outer qualifier by passing the reference as a fresh argument (by t-app-
fresh ):
valinner = ... // : Tinner
valc1 = newRef(inner) // : (Ref[Tinner])c1,inner
valc2 = newRef(inner) // : (Ref[Tinner])c2,inner
defnewctx(c1' : Ref[Tinner]q)(c2' : Ref[Tinner]q) = {
// attempt to use c1' and c2' as separate resource, okay
}
However, the function can never be invoked with the desired argument c1andc2, because the
function demands the two separate references to contain a shared value inner, which is prohibited,
as illustrated in Figure 2b. Semantically, the resulting function of partial application of the first
argument c1captures inner, which overlaps with the second argument c2, but the function signature
requires c2to be a contextually fresh argument:
newctx(c1)(c2) // Error: newctx(c1) has overlapping qualifier ‘inner‘ with c2
In other words, in Wei et al .[2024], reference qualifiers are saturated tracking their transitively
reachable store locations. Consequently, as illustrated in Figure 2b, individually fresh references
must not reach shared store locations.
To address this constraint, we disentangle the reference qualifier and the referent qualifier,
removing the inclusion requirement on the outer reference qualifier. Now consider the same
example shown in Section 1:
vala = ... // : Ta
valcell = newRef(a) // : (Ref[Ta])cell
// a and cell are distinct locations now
Page 10:
10 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
cell := ... // (cell, use)
// Good: cell is used without affecting a
Note that the qualifier of cellno longer contains the qualifier of its referent, a, in this case. This
allows the type system to attain a higher precision and express separation between the reference
and the referent, and aligns reference typing to the one-step reachability model.
The shallow tracking mechanism we propose scales well to nested references. Figure 2c shows
that references capturing the same resource are correctly treated as separate.
3𝜆◦
<:: Reachability Types with Cyclic Reference Type
In this section, we formally define 𝜆◦
<:and prove key theorems to establish its type safety proof.
We use Wei et al .[2024] as a base system, highlighting additions in gray boxes . When appropriate,
we also use gray color to indicate typing rules in 𝜆qthat are superseded by new rules in 𝜆◦
<:and no
longer present in the system, aligning them side-by-side for easy comparison.
3.1 Syntax
We propose a cyclic reference type in the form of 𝝁𝑥.Ref[𝑇𝑞]𝑝. Intuitively, 𝝁𝑥creates a bound
variable𝑥that can appear in 𝑞to refer to its outer qualifier 𝑝. The bound variable has a more
significant meaning in the context of dereferencing (Section 3.2.2) and assignment (Section 3.2.3),
which we defer to their corresponding sections.
For any reference 𝝁𝑥.Ref[𝑇𝑞]𝑝, when there is no bound variable 𝑥present in the referent
qualifiers𝑞, it is a non-cyclic reference , and can be abbreviated into Ref[𝑇𝑞]𝑝, which we adopt
from Wei et al .[2024] as syntactic sugar (See Figure 4). When the bound variable 𝑥iscontained in
the referent qualifier 𝑞, the full 𝝁𝑥notation must be used to avoid ambiguity.
Although the 𝝁𝑥notation we use coincides with other systems such as recursive types ([Abadi
and Fiore 1996; Pierce 2002]) and DOT ([Amin et al .2016; Rompf and Amin 2016]), cyclic references
denoted by 𝝁𝑥have distinct meaning unlike that of other works, and we elaborate on the difference
in Section 5.
3.2 Static Typing
We now discuss details regarding the typing rules for 𝜆◦
<:.t-var andt-cst are typing rules for
variables and constants. While the former provides typing for free variables in the context, the
latter provides typing for base types. For this section, we assume Unit is the only base type in the
system. We include natural numbers and boolean types as base types in Section 4.
3.2.1 Introduction Rules. t-sref andt-sref-2 are introduction rules for the reference type, con-
structing non-cyclic references and cyclic references respectively. Like t-ref ,t-sref creates non-
cyclic references, but it removes the deep dependency between the inner and the outer qualifiers.
Specifically, the reference constructor does not propagate the referent qualifier ( e.g.q) to the outer
qualifier. We maintain a shallow dependency, making the outer qualifier always track precisely
what is reached by the reference itself without the resource contained within it. This modifies the
interpretation of reference qualifiers from Wei et al .[2024]. Instead of tracking all the transitively
reachable locations through the store typing, the reference qualifier only reaches the underlying
location (see Section 2.4).
Similar to Wei et al .[2024], we disallow creating references to fresh resources to ensure sound
reachability tracking, preventing imprecise aliasing tracking. Without this restriction, dereferencing
(see Section 3.2.2) such a reference multiple times would produce values that, from the qualifier’s
perspective, appear to be distinct fresh resources while actually referring to the same underlying
resource.
Page 11:
Complete the Cycle: Reachability Types with Expressive Cyclic References 11
Syntax 𝜆◦<:𝑥,𝑦,𝑧∈ Var Variables
𝑓,𝑔,ℎ∈ Var Function Variables
𝑋∈ Var Type Variables
𝑆,𝑇,𝑈,𝑉 ::= Unit|𝑓(𝑥:𝑄)→𝑅|𝝁𝑥.Ref[𝑄]
|Top|𝑋|∀𝑓(𝑋𝑥<:𝑄).𝑄 Types
𝐵 ::= Unit Base Types
𝑡 ::=𝑐|𝑥|𝜆𝑓(𝑥).𝑡|𝑡𝑡|ref𝑡|!𝑡|𝑡B𝑡
|Λ𝑓(𝑋𝑥).𝑡|𝑡[𝑄] Terms
𝑝,𝑞,𝑟,𝑤∈ P fin(Var⊎{q}) Type Qualifiers
𝑂,𝑃,𝑄,𝑅 ::=𝑇𝑞Qualified Types
𝜑∈ P fin(Var) Observations
Γ ::=∅|Γ,𝑥:𝑄|Γ,𝑋𝑥<:𝑄 Typing Environments
Reference Notations
Ref[𝑄]:=𝝁𝑥.Ref[𝑄] if𝑥∉fv(𝑄)
Qualifier Notations
𝑝,𝑞 :=𝑝∪𝑞 Qualifier Union
𝑞⊖𝑥 :=𝑞\{𝑥} Qualifier Exclusion
𝑥 :={𝑥} Single Variable Qualifier
q :={q} Single Fresh Qualifier
{Var} :={{𝑥}|𝑥∈Var} Singleton Variable Qualifiers
P1 :={Var} Singleton Qualifiers
Fig. 4. The syntax of 𝜆◦<:.
3.2.2 Dereference Rules. The dereference rule ( t-sderef ) serves as the elimination form for refer-
ence types, ensuring that the dereference operation ( !...) correctly retrieves the stored referent
while preserving its typing and qualifier. A key subtlety in handling the referent qualifier is that,
in addition to returning the inner qualifier 𝑞, we substitute the bound variable using the outer
qualifier𝑝. This substitution is necessary because the bound variable acts as an abstraction for
the outer qualifier within the reference type. Once dereferencing eliminates the reference type,
this abstraction must be replaced with the actual outer qualifier, as the resulting value no longer
contains a reference and thus cannot retain the abstraction.
For non-cyclic references, where the bound variable xis absent from the referent qualifier, this rule
generalizes the t-deref rule in Wei et al .[2024], simply retrieving the referent qualifier. However,
for cyclic references where the referent qualifier contains the bound variable x, the operation must
retrieve both the referent qualifier and the reference qualifier, by substituting the bound variable
with the outer qualifier. Thus, the bound variable serves as a abstraction for the outer qualifier.
Through dereferencing, we concretize this abstraction, making the outer reference qualifier explicit
in the resulting type. However, such an abstraction is limited in that the bound variables can refer
only to their immediate outer qualifier, rather than qualifiers at arbitrary depth, as seen in lambda
abstractions (see Section 6).
3.2.3 Assignment Rules. Assignment updates the value stored in a mutable reference. Due to the
complexities of assigning to cyclic references, we introduce two distinct assignment rules.
Page 12:
12 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
Term Typing Γ𝜑⊢𝑡:𝑄
𝑦:𝑇𝑞∈Γ𝑦∈𝜑
Γ𝜑⊢𝑦:𝑇𝑦(t-var)𝑐∈𝐵
Γ𝜑⊢𝑐:𝐵∅(t-cst)
Γ𝜑⊢𝑡:𝑇𝑞q∉𝑞
Γ𝜑⊢ref𝑡:(Ref𝑇𝑞)𝑞,q
(t-ref)Γ𝜑⊢𝑡:𝑇𝑞q∉𝑞
Γ𝜑⊢ref𝑡:(Ref𝑇𝑞)q
(t-sref)Γ𝜑⊢𝑡:𝑇𝑞q∉𝑞
Γ𝜑⊢ref𝑡:𝝁𝑥.Ref[𝑇𝑥,𝑞]q
(t-sref-2)
Γ𝜑⊢𝑡:(Ref𝑇𝑞)𝑝𝑞⊆𝜑
Γ𝜑⊢!𝑡:𝑇𝑞
(t-deref)Γ𝜑⊢𝑡:𝝁𝑥.Ref[𝑇𝑞]𝑝𝑞⊆𝜑,𝑥𝑥∉fv(𝑇)
Γ𝜑⊢!𝑡:𝑇𝑞[𝑝/𝑥](t-sderef)
Γ𝜑⊢𝑡1:(Ref𝑇𝑞)𝑝
Γ𝜑⊢𝑡2:𝑇𝑞q∉𝑞
Γ𝜑⊢𝑡1B𝑡2:Unit∅
(t-assgn)Γ𝜑⊢𝑡1:𝝁𝑥.Ref[𝑇𝑞]𝑝
Γ𝜑⊢𝑡2:𝑇𝑞⊖𝑥
Γ𝜑⊢𝑡1B𝑡2:Unit∅
(t-sassgn)Γ𝜑⊢𝑦:𝝁𝑥.Ref[𝑇𝑞,𝑥]𝑝
Γ𝜑⊢𝑡2:𝑇𝑦,𝑞
Γ𝜑⊢𝑦B𝑡2:Unit∅
(t-sassgn-v)
Γ𝜑⊢𝑡1:(𝑓(𝑥:𝑇𝑝)→𝑈𝑟)𝑞
Γ𝜑⊢𝑡2:𝑇𝑝q∉𝑝
𝑟⊆q,𝜑,𝑥,𝑓𝑝∉P1⊎{∅}⇒𝑥∉fv(𝑈)
Γ𝜑⊢𝑡1𝑡2:𝑈𝑟[𝑝/𝑥,𝑞/𝑓]
(t-app)Γ𝜑⊢𝑡1: 𝑓(𝑥:𝑇𝑝
q∩𝑞)→𝑈𝑟𝑞Γ𝜑⊢𝑡2:𝑇𝑝
q∈𝑝⇒𝑥∉fv(𝑈)q∈𝑞⇒𝑓∉fv(𝑈)
𝑟⊆q,𝜑,𝑥,𝑓𝑝∉P1⊎{∅}⇒𝑥∉fv(𝑈)
Γ𝜑⊢𝑡1𝑡2:(𝑈𝑟)[𝑝/𝑥,𝑞/𝑓]
(t-app-fresh)
(Γ, 𝑓:𝐹 , 𝑥 :𝑃)𝑞,𝑥,𝑓⊢𝑡:𝑄
𝐹=(𝑓(𝑥:𝑃)→𝑄)𝑞𝑞⊆𝜑
Γ𝜑⊢𝜆𝑓(𝑥).𝑡:𝐹
(t-abs)(Γ, 𝑓:𝐹 , 𝑋𝑥<:𝑃)𝑞,𝑥,𝑓⊢𝑡:𝑄
𝐹=(∀𝑓(𝑋𝑥<:𝑃).𝑄)𝑞𝑞⊆𝜑
Γ𝜑⊢Λ𝑓(𝑋𝑥).𝑡:𝐹
(t-tabs)Γ𝜑⊢𝑡:𝑄 Γ⊢𝑄<:𝑇𝑞
𝑞⊆𝜑,q
Γ𝜑⊢𝑡:𝑇𝑞
(t-sub)
Γ𝜑⊢𝑡:(∀𝑓(𝑋𝑥<:𝑇𝑝).𝑄)𝑞
q∉𝑝 𝑓∉fv(𝑈)
𝑝⊆𝜑 𝑟⊆
q𝜑,𝑥,𝑓 𝑄 =𝑈𝑟
Γ𝜑⊢𝑡[𝑇𝑝]:𝑄[𝑇𝑝/𝑋𝑥,𝑞/𝑓](t-tapp)Γ𝜑⊢𝑡: ∀𝑓(𝑋𝑥<:𝑇𝑝
q∩𝑞).𝑄𝑞
q∈𝑝⇒𝑥∉fv(𝑈)𝑓∉fv(𝑈)
𝑝⊆𝜑 𝑟⊆
q𝜑,𝑥,𝑓 𝑄 =𝑈𝑟
Γ𝜑⊢𝑡[𝑇𝑝]:𝑄[𝑇𝑝/𝑋𝑥,𝑞/𝑓](t-tapp-fresh)
Fig. 5. Typing rules of 𝜆◦<:. Differences from Wei et al .[2024] are highlighted in gray boxes . The gray
rules are directly taken from Wei et al. [2024] for comparison purposes, and are not a part of 𝜆◦<:.
t-sassgn applies only when the assigned term’s qualifier does not refer to the assignee itself.
When the assignee is a non-cyclic reference, the assignment rule follows the same semantics as
t-assgn in Wei et al .[2024]’s system. Unlike t-assgn , which applies only to non-cyclic references,
t-sassgn generalizes assignment to cyclic references as well. As a consequence, when assigning
to a cyclic reference, the bound variable xin its referent qualifier is ignored. To ensure that the
assigned term remains well-formed, the bound variable must not appear in the qualifier of the
assigned term ( 𝑞⊖𝑥).
Fort-sassgn-v , the assignee must be a cyclic reference. In this case, assignment becomes more
complex, as it allows values to reach the reference’s outer qualifier. The system permits this
assignment only when the assignee is a single variable and the assigned term has a singleton
qualifier matching the assignee’s name. Allowing assignment without enforcing a variable-form
assignee and a matching singleton qualifier, as in t-sassgn-err (see Section 2.2), would enable
assignments with arbitrary qualifiers, violating the intended type discipline. This is because q-sub
allows arbitrary upcasting of a reference’s outer qualifier, and including a rule like t-sassgn-err
would lead to inconsistencies in qualifier tracking.
Page 13:
Complete the Cycle: Reachability Types with Expressive Cyclic References 13
Subtyping Γ⊢𝑞<:𝑞Γ⊢𝑇<:𝑇Γ⊢𝑄<:𝑄
Γ⊢𝐵<:𝐵(s-base)
Γ⊢𝑇<:𝑆Γ⊢𝑆<:𝑈
Γ⊢𝑇<:𝑈(s-trans)Γ⊢𝑆<:𝑇Γ⊢𝑇<:𝑆 𝑞⊆dom(Γ)
Γ⊢𝝁𝑧.Ref[𝑆𝑝]𝑞<:𝝁𝑧.Ref[𝑇𝑝]𝑞(s-ref)
Γ⊢𝑃<:𝑂
Γ, 𝑓:(𝑓(𝑥:𝑂)→𝑄)q,𝑥:𝑃⊢𝑄<:𝑅
Γ⊢𝑓(𝑥:𝑂)→𝑄<:𝑓(𝑥:𝑃)→𝑅(s-fun)
𝑝⊆𝑞⊆
qdom(Γ)
Γ⊢𝑝<:𝑞(q-sub)
Γ⊢𝑞1<:𝑞2
Γ⊢𝑝,𝑞1<:𝑝,𝑞2(q-cong)𝑓:𝑇𝑞∈Γq∉𝑞
Γ⊢𝑞,𝑓<:𝑓(q-self)
𝑥:𝑇𝑞∈Γq∉𝑞
Γ⊢𝑥<:𝑞(q-var)𝑋𝑥<:𝑇𝑞∈Γq∉𝑞
Γ⊢𝑝,𝑥<:𝑝,𝑞(q-qvar)
𝑋𝑥<:𝑇𝑞∈Γ
Γ⊢𝑋<:𝑇(s-tvar)
Γ⊢𝑝<:𝑞Γ⊢𝑞<:𝑟
Γ⊢𝑝<:𝑟(q-trans)Γ⊢𝑆<:𝑇 Γ⊢𝑝<:𝑞
Γ⊢𝑆𝑝<:𝑇𝑞(sq-sub)
Fig. 6. Subtyping rules of 𝜆◦<:.
Transitive Lookup 𝑞{𝑛
Γ𝑞{Γ
𝑞{0
Γ:=𝑞 Qualifier Zero-step Transitive Lookup
𝑞{1
Γ:=Ð
(𝑥∈𝑞∧𝑥:𝑇𝑝∈Γ)𝑝∪𝑞 Qualifier One-Step Transitive Lookup
𝑞{𝑛+1
Γ:=(𝑞{1
Γ){𝑛
ΓQualifier Multi-Step Transitive Lookup
𝑞{Γ:=𝑞{|Γ|
ΓQualifier Full Transitive Lookup
Qualifier Notations
satΓ𝑞 :=𝑞{Γ=𝑞
Qualifier Saturation
Γ⊢𝑝
q∩𝑞:=
q(𝑝{Γ∩𝑞{Γ)
Qualifier OverlapQualifier Cardinality |𝑞|Γ
|𝑞|∅ :=0
|𝑞|(Γ,𝑥:𝑄):=1+|𝑞|Γ if𝑥∈𝑞
|𝑞|(Γ,𝑥:𝑄):=|𝑞|Γ otherwise
Fig. 7. Qualifier Transitive Lookup.
Why, then, is it safe to restrict assignment to term forms that are variables? By t-var , a variable
is always assigned a singleton qualifier that matches its name. Although this variable’s qualifier can
be upcasted arbitrarily, the singleton qualifier is its most precise tracking prior to any upcasting.
Thus, restricting the assigned term’s qualifier to a matching singleton ensures that it refers to the
intended reference and cannot be widened to include other resources.
In summary, for cyclic reference assignment, we determine the assigned term’s qualifier based
on the assignee’s term form, rather than its qualifier. Unlike qualifiers, which can be upcasted, term
forms remain fixed, ensuring correctness in assignment. We find that t-sassgn-v achieves a balance
between correctness and precision while successfully supporting cyclic reference assignment.
3.2.4 Application Rules. Similar to Wei et al .[2024],𝜆◦
<:defines two variants of the application
rule: t-app for precise applications ( i.e.“non-fresh”) and t-app-fresh for growing applications ( i.e.
“fresh”).
Page 14:
14 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
Term Typing (with Store Typing) [Γ|Σ]𝜑⊢𝑡:𝑄
ℓ∈ Loc Locations
𝑡 ::=···|ℓ Terms
𝑣 ::=𝜆𝑓(𝑥).𝑡|𝑐|ℓ|unit|Λ𝑓(𝑋𝑥).𝑡 Values
𝑝,𝑞,𝑟∈ P fin(Var⊎Loc⊎{q}) Qualifiers
𝜑∈ P fin(Var⊎Loc) Observations
Σ ::=∅|Σ,ℓ:𝑇𝑞|Σ,ℓ:𝝁𝑥.𝑇𝑞,𝑥Store Typing
{Loc} :={{ℓ}|ℓ∈Loc} Singleton Location Qualifiers
P1 :={Var}⊎{ Loc} Singleton Qualifiers
Σ(ℓ)=𝑇𝑞𝑞⊆dom(Σ)
fv(𝑇)=∅ftv(𝑇)=∅𝑞,ℓ⊆𝜑
[Γ|Σ]𝜑⊢ℓ:Ref[𝑇𝑞]ℓ(t-loc)Σ(ℓ)=𝝁𝑥.𝑇𝑞,𝑥𝑞⊆dom(Σ)
fv(𝑇)=∅ftv(𝑇)=∅𝑞,ℓ⊆𝜑
[Γ|Σ]𝜑⊢ℓ:𝝁𝑥.Ref[𝑇𝑞,𝑥]ℓ(t-sloc)
[Γ|Σ]𝜑⊢𝑡1:(𝑓(𝑥:𝑇𝑝)→𝑄)𝑞
[Γ|Σ]𝜑⊢𝑣:𝑇𝑝𝑄=𝑈𝑟
𝑟⊆q,𝜑,𝑥,𝑓𝑝∉P1⊎{∅}⇒𝑣≠ℓ
[Γ|Σ]𝜑⊢𝑡1𝑣:𝑄[𝑝/𝑥,𝑞/𝑓]
(t-app-val)[Γ|Σ]𝜑⊢ℓ:𝝁𝑥.Ref[𝑇𝑞]𝑝,ℓ
[Γ|Σ]𝜑⊢𝑡2:𝑇𝑞,ℓq∉𝑞 𝑥∈𝑞
[Γ|Σ]𝜑⊢𝑡1B𝑡2:Unit∅
(t-sassgn-l)
Well-Formed Stores Σok
∅ok(st-emp)Σok fv(𝑇)=∅ftv(𝑇)=∅𝑞∈dom(Σ)ℓ∉dom(Σ)
Σ, ℓ:𝑇𝑞ok(st-con)
Σok fv(𝑇)=∅ftv(𝑇)=∅𝑞∈dom(Σ)ℓ∉dom(Σ)
Σ,ℓ:𝝁𝑥.𝑇𝑞,𝑥ok(st-scon)
Reduction Contexts, Stores
𝐶::=□|𝐶𝑡|𝑣𝐶|ref𝐶|!𝐶|𝐶:=𝑡|𝑣:=𝐶|𝐶[𝑄]𝜎::=∅|𝜎,ℓ↦→𝑣
Reduction Rules 𝑡|𝜎→𝑡|𝜎
𝐶[(𝜆𝑓(𝑥).𝑡)𝑣]|𝜎→𝐶[𝑡[𝑣/𝑥,(𝜆𝑓(𝑥).𝑡)/𝑓]]|𝜎 (𝛽)
𝐶[ref𝑣]|𝜎→𝐶[ℓ]|(𝜎,ℓ↦→𝑣) ℓ∉dom(𝜎) ( ref)
𝐶[!ℓ]|𝜎→𝐶[𝜎(ℓ)]|𝜎 ℓ ∈dom(𝜎) ( deref)
𝑡𝐶[ℓ:=𝑣]|𝜎→𝐶[unit]|𝜎[ℓ↦→𝑣] ℓ∈dom(𝜎) ( assign)
𝐶[(Λ𝑓(𝑋𝑥).𝑡)𝑄]|𝜎→𝐶[𝑡][𝑄/𝑋𝑥,(Λ𝑓(𝑋𝑥).𝑡)/𝑓]|𝜎 (𝛽𝑇)
Fig. 8. Extension with store typings and call-by-value reduction for 𝜆◦<:. Store typing for cyclic references
are highlighted in gray boxes . In contrast to Wei et al .[2024], we do not require saturated qualifiers
on well-formed stores.
t-app applies to non-fresh applications, where the argument’s qualifier is fully observable and
explicitly specified. In this case, the function return type can depend on the function argument
qualifier, and the application performs a deep, precise substitution on the argument qualifier. To
ensure correct deep substitution of qualifiers in the presence of cyclic references, we impose an
additional constraint: the argument qualifier must not appear in the return type, unless it belongs
to a restricted set of qualifiers – optional singleton qualifiers ( i.e.∈P 1⊎∅) – which permit deep
substitution.
Page 15:
Complete the Cycle: Reachability Types with Expressive Cyclic References 15
If the argument does not appear in the return type, type preservation is trivially maintained
since no type-level substitution is required. If the argument qualifier does appear in the return type,
it must be an optional singleton to ensure valid deep substitution. Allowing deep substitution of
non-singleton qualifiers in function return types could lead to inconsistent typing, violating type
preservation (see Section 3.5). This constraint limits expressiveness but is necessary to preserve
type soundness. We further justify this limitation in Section 6.2.
Deep substitution remains valid under the following cases, where the argument qualifier is:
(1) an empty qualifier ( 𝑝∈{∅} ), or
(2) a singleton qualifier ( 𝑝∈P 1).
Thus, when the argument qualifier is an optional singleton, deep substitution in t-app remains
valid because the qualifier is small enough to be directly substituted using the substitution lemma.
t-app-fresh extends the constraints of t-app to fresh applications, enforcing the same non-
occurrence constraint when the qualifier is not an optional singleton. Additionally, a similar
restriction applies to applications involving store locations (see Section 3.3).
3.2.5 Type Polymorphism. t-tapp andt-tapp-fresh extend the type application rule to support
type and qualifier polymorphism, where a type abstraction can be typed with t-tabs . Unlike
function applications, type applications impose no restrictions on the argument qualifier, as types
do not appear on the left-hand side of assignment operations, eliminating concerns about improper
substitution.
3.3 Dynamic Typing
The𝜆◦
<:-calculus follows standard call-by-value reduction for the 𝜆-calculus with mutable references.
A store and a store typing track the values, types, and qualifiers associated with each location.
References reduce to fresh locations with their types and qualifiers recorded in the store typing
(seet-loc andt-sloc ). Assignment statements evaluate to a unit value while updating the store.
Additionally, t-sassgn-l introduces a dynamic typing rule for cyclic assignments, where the
assignee is a single location.
Function applications reduce to the function body via 𝛽-reduction, replacing occurrences of
the function argument with a concrete value. t-app-val extends typing to applications within
abstraction bodies at runtime, where an argument variable is substituted with a value. As in t-app ,
the optional singleton qualifier constraint applies to argument qualifiers. Singleton qualifiers now
also extend to singleton location qualifiers (see Figure 8).
When the argument qualifier is notan optional singleton, the argument must not be a single
location, as demanded by the substitution lemma (see Section 3.5.2). The call-by-value semantics
allows us to relax the static typing constraint on the non-occurrence of the argument qualifier in the
function’s return type ( i.e.𝑥∉fv(𝑈)), as per t-app . Instead, we impose a weaker requirement: the
argument must not be a location value ( i.e.𝑣≠ℓ). This restriction prevents improper substitution by
ensuring locations always have their corresponding singleton qualifier when applied to abstractions.
In contrast, static typing must impose the non-occurrence constraint because arguments may
include arbitrary terms beyond values, and their types may involve type abstractions, which cannot
be checked syntactically.
Unlike𝜆q,𝜆◦
<:drops the saturation constraint for qualifiers in the store, extending store typing
to support both cyclic references and non-cyclic references.
3.4 Precise Transitive Closure Computation
In Wei et al .[2024]’s mechanization, the concept of transitive closure is expressed indirectly via
a “saturation” predicate, which specifies that a qualifier will reach no more than itself through
Page 16:
16 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
the corresponding store. In conjunction with universal quantification, one can approximate the
transitive closure of qualifier 𝑝as asaturated superset of a𝑝.
We revise this definition by redefining the transitive closure deterministically , using a “fuel” value
that is set to the store length to ensure termination and facilitate reasoning, even in the presence
of circular pointers in the context and store typing. We argue that this approach is more precise
since it pinpoints the exact qualifier instead of specifying a range of qualifiers that is larger than
its transitive closure. Although it is possible to make the above definition precise by specify the
transitive closure as the smallest saturated superset of a qualifier, it involves second order universal
quantification, and can complicate both the specification and the reasoning process.
The transitive closure computation is generalized over both the context and the store typing,
allowing code reuse in both t-app-fresh and the preservation of separation lemma. We define
standard commutativity and distributivity of the transitive closure with respect to other operations
on sets and qualifiers ( e.g.splice, substitution, etc.). We show that the computational definition
subsumes the saturation by redefining the saturation predicate using the deterministic transitive
closure computation.
3.5 Metatheory
3.5.1 Transitive Closure Computation. We define the concept of cardinality on qualifiers to capture
the number of variables that is contained in a qualifier (See Section 3). Using cardinality, we establish
a mapping between cardinality and qualifier saturation.
Lemma 3.1 (Cardinality Monotonicity). If𝑞1⊆𝑞2, then|𝑞1|Γ≤|𝑞2|Γ.
Proof. By induction on the typing environment, with case analysis in the inductive case on
whether the qualifier contains the top element. □
Lemma 3.2 (Cardinality Max). |𝑞|Γ≤|Γ|.
Proof. By induction on the typing environment, with case analysis in the inductive case on
whether the qualifier contains the top element. □
Lemma 3.3 (Zero Cardinality Saturated). If|𝑞|Γ=0, Then satΓ𝑞.
Proof. By induction on Γ. □
Lemma 3.4 (Cardinality and Sub-qalifier Preservation). If|𝑞1|Γ=|𝑞1∪𝑞2|Γ, then𝑞1{1
Γ
∪𝑞2{1
Γ=𝑞1{1
Γ∪𝑞2.
Proof. By Lemma 3.1, we have |𝑞1|Γ≤|𝑞1∪𝑞2|Γ, By induction on the typing environment and
with case analysis on whether the qualifiers contain the top element, in each case we either apply
the induction hypothesis or derive a contradiction. □
Lemma 3.5 (Transitive Lookup Monotone). 𝑞⊆Γ{𝑞
𝑛.
Proof. By induction on 𝑛. □
Lemma 3.6 (Cardinality Increment or Saturation). If𝑞′=𝑞{Γ𝑛, then|𝑞|Γ+𝑛≤|𝑞′|Γor
satΓ𝑞′.
Proof. We first prove the case for 𝑛=1and then proceed by induction on 𝑛. For the base case,
we use Lemma 3.5 and Lemma 3.1 to establish the left disjunct. For the inductive step, we apply the
induction hypothesis and then invoke the case for 𝑛=1. □
Lemma 3.7 (Full Transitive Lookup Total). If𝑛≥|Γ|, then𝑞{𝑛
Γ=𝑞{|Γ|
Γ.
Page 17:
Complete the Cycle: Reachability Types with Expressive Cyclic References 17
Proof. Applying Lemma 3.6 to 𝑞with𝑛, we consider two cases:
(1) Cardinality is increasing: This contradicts Lemma 3.2.
(2)𝑞is saturated: We analyze the cardinality value:
•If it is zero, we apply Lemma 3.3.
•If it is nonzero, we apply Lemma 3.2 to derive a contradiction.
□
3.5.2 Substitution Lemma.
Lemma 3.8 (Substitution preserves transitive lookup). If𝑥:𝑇𝑞∈Γ, and𝑝,𝑞⊆
qdom(Σ),
and𝑝∩
q𝜑⊆𝑞, and𝑟{Γ⊆
q𝜑, then under substitution 𝜃=[𝑝/𝑥],
𝑟𝜃{Γ𝜃⊆𝑟{Γ𝜃.
Proof. We proceeds by applying transitivity of subtyping, followed by commutativity of transi-
tive lookup under substitution, monotonicity of qualifier substitution, and environment weakening
properties. The proof concludes by applying subqualifier transitivity and narrowing arguments. □
Lemma 3.9 (Top-Level Term Substitution). Suppose the following typing judgments hold:
[𝑥:𝑇𝑞,Γ|Σ]𝜑⊢𝑡:𝑄,[∅|Σ]𝑝⊢𝑣:𝑇𝑝.
Additionally, assume:
𝑝,𝑞⊆
qdom(Σ),
𝑝∩
q𝜑⊆𝑞,
𝑞=𝑝∨𝑞=
q(𝑝∩𝑟)∨(𝑞=ℓ∨𝑞=
q(ℓ∩𝑟))∧𝑇=𝝁𝑥.Ref[𝑈𝑤]𝑝,
(∃ℓ,𝑣=ℓ)→𝑝=ℓ.
Then, under substitution 𝜃=[𝑝/𝑥], we have:
[Γ𝜃|Σ]𝜑𝜃⊢𝑡[𝑣/𝑥]:𝑄𝜃.
Proof. We proceed by induction on the derivation [𝑥:𝑇𝑞,Γ|Σ]𝜑⊢𝑡:𝑄.
In the case of t-app-fresh , the induction hypothesis requires Lemma 3.8 to establish (𝑝
q∩𝑞)𝜃⊆
𝑝𝜃
q∩𝑞𝜃.
In the case of t-sassgn-v , we perform case analysis on the variable assignee. If the variable is
the one being substituted, we use the fact that the substituted value is a reference, allowing us to
conclude that it is a location. We then apply t-sassgn-l to complete the case. If the variable is
different from the one being substituted, the proof follows directly from the induction hypothesis.
Other cases follow straightforwardly from the induction hypothesis. □
The condition
𝑞=𝑝∨𝑞=
q(𝑝∩𝑟)∨(𝑞=ℓ∨𝑞=
q(ℓ∩𝑟))∧𝑇=𝝁𝑥.Ref[𝑈𝑤]𝑝
captures the four possible cases of substitution:
(1)Precise substitution (𝑞=𝑝): The assumed qualifier 𝑞for𝑥matches the value’s qualifier 𝑝.
This occurs for function parameters in t-app or for a function’s self-reference 𝑓int-app
andt-app-fresh .
(2)Growing substitution (𝑞=
q(𝑝∩𝑟)): This applies in t-app-fresh , where the argument
qualifier𝑝overlaps with the function qualifier 𝑟, growing the result by 𝑝\𝑟{Γ.
(3)Precise substitution with a location qualifier (𝑞=ℓ): A single location qualifier can be used
similarly to case (1).
Page 18:
18 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
(4)Growing substitution with a location qualifier (𝑞=
q(ℓ∩𝑟)): Analogous to case (2), but using
a location qualifier.
Cases (3) and (4) apply only when the argument type is a reference type.
Since cyclic assignment ( t-sassgn-v ) can occur inside an abstraction body, if the assigned
term’s qualifier contains the function argument qualifier, the latter must be substituted with an
optional singleton qualifier to ensure that the cyclic assignment remains well-typed after qualifier
substitution.
As we consider only top-level, closed values in substitution, this constraint becomes relevant only
when the substituted term is a location value ( e.g.ℓ), as it could potentially serve as the assignee in
a cyclic assignment operation. This requirement is captured by the premise (∃ℓ,𝑣=ℓ)→𝑝=ℓ.
3.5.3 Main Soundness Result.
Theorem 3.10 (Progress). If[∅|Σ]𝜑⊢𝑡:𝑄andΣok, then either 𝑡is a value, or for any store
𝜎where[∅|Σ]𝜑⊢𝜎, there exists a term 𝑡′and store𝜎′such that𝑡|𝜎→𝑡′|𝜎′.
Proof. By induction over the derivation [∅|Σ]𝜑⊢𝑡:𝑄. □
Similar to [Wei et al. 2024], reduction preserves types up to qualifier growth:
Theorem 3.11 (Preservation). If[∅|Σ]𝜑⊢𝑡:𝑇𝑞, and[∅|Σ]𝜑⊢𝜎, and𝑡|𝜎→𝑡′|𝜎′,
andΣok, then there exists Σ′⊇Σ,𝜑′⊇𝜑∪𝑝, and𝑝⊆dom(Σ′\Σ)such that[∅|Σ′]𝜑′⊢𝜎′and
[∅|Σ′]𝜑′⊢𝑡′:𝑇𝑞[𝑝/q].
Proof. We proceed by induction on the derivation [∅|Σ]𝜑⊢𝑡:𝑇𝑞.
Fort-app , we distinguish two cases:
1. If the argument qualifier is an optional singleton, we apply the substitution lemma directly
using the typing derivation from the hypothesis.
2. If the argument qualifier is larger than an optional singleton, we first derive the non-occurrence
assumption for the argument qualifier in the function return type. This ensures that the return
qualifier remains preserved after stepping. We then construct a separate typing derivation for 𝑡
with a qualifier 𝑤that is more precise than 𝑝. In particular, if 𝑡is a location ℓ, then𝑟=ℓ. Using this
refined typing derivation, we apply the substitution lemma (Lemma 3.9), thereby completing the
case. □
Corollary 3.12 (Preservation of Separation). Sequential reduction of two terms with disjoint
qualifiers preserve types and disjointness:
[∅|Σ]dom(Σ)⊢𝑡1:𝑇𝑞1
1𝑡1|𝜎→𝑡′
1|𝜎′∅|Σ⊢𝜎 Σok
[∅|Σ]dom(Σ)⊢𝑡2:𝑇𝑞2
2𝑡2|𝜎′→𝑡′
2|𝜎′′𝑞1
q∩𝑞2⊆{q}
∃𝑝1𝑝2Σ′Σ′′.[∅|Σ′]dom(Σ′)⊢𝑡′
1:𝑇𝑝1
1Σ′′⊇Σ′⊇Σ
[∅|Σ′′]dom(Σ′′)⊢𝑡′
2:𝑇𝑝2
2𝑝1
q∩𝑝2⊆{q}
Proof. By sequential application of Preservation (Theorem 3.11) and the fact that a reduction step
increases the assigned qualifier by at most a fresh new location, thus preserving disjointness. □
The Progress and Preservation in Parallel Reduction corollary is ommitted due to space limitation.
Page 19:
Complete the Cycle: Reachability Types with Expressive Cyclic References 19
4 Case Study: A Fixed-point Combinator
In this section, we present a case study demonstrating how cyclic reference types enable the
implementation of a general fixpoint operator, allowing functions to define themselves recursively
without explicit recursion.
As in system Fq
<:, our system supports type polymorphism, allowing functions and references to
be parameterized over types while ensuring type safety. We implement a general fixpoint operator
through the store, following Kiselyov [2020]. The fixpoint operator is defined as follows:
deffix[T] (f: (g: (T -> T)q-> (T -> T)g)) : (T -> T)q= {
valc = newRef (x => x) // : 𝝁𝑧.Ref[(T -> T)z]c
c := f((n:T) => (!c)(n)) // : (T -> T)c
!c
}
The key idea is to use a reference to hold the function being defined recursively, ensuring that it
can be updated as needed. The fixpoint operator is polymorphic over type T, making it applicable to
recursive computations on arbitrary data types. The function fis a higher-order function passed as
an argument to the fixpoint operator, performing a “one-step” computation, using its first argument
g(of type T -> T ) as the function that it refines recursively.
Within the function body, we complete the recursive definition by performing the following
steps:
(1)Initializing the cyclic reference ( c).We create a reference cof typeT -> T , initially
holding the identity function (x => x) as a placeholder, ensuring type correctness and that
the reference can be safely dereferenced before being updated.
(2)Defining the helper function ( f2).The function f2is a wrapper around c, retrieving its
current value ( !c) and applying it to the argument n. Sincecwill later be updated to hold
the final recursive function, f2essentially acts as a proxy to dynamically retrieve and apply
the most up-to-date version of the function.
(3)Updating cwith the recursive function. We apply ftof2, allowing fto construct the
recursive function by invoking f2as needed. The result of this computation ( f(f2) ) is then
stored in c, ensuring f2retrieves the updated definition at the next recursive step.
(4)Returning the fixpoint. The fixpoint operator finally returns the dereferenced value of c,
which now holds the fully-defined recursive function. Any subsequent calls to the function
returned by fixwill now correctly apply the recursively computed function.
Unlike explicit recursive definitions, this approach enables recursion through mutable, cyclic
references, allowing functions to be defined incrementally. This makes it particularly useful in
settings where recursion needs to be established dynamically, such as in languages without native
support for recursion or when defining mutually recursive functions.
One possible instantiation of the fixpoint operator is an infinite loop. In this case, the fixpoint oper-
ator is instantiated with type Unit, and the “one-step” computation is a function that unconditionally
applies its first argument to its second argument.
defloop_fix[Unit](g: Unit -> Unit): Unit -> Unit = n => g(n)
fix[Unit](loop _fix)(()) // infinite loop
To demonstrate more practical use cases than infinite loops, we extend the system with integer
types and basic arithmetic operations (see Figure 9), enabling us to define a factorial function using
the fixpoint operator:
deffact_fix(f: Nat -> Nat): Nat -> Nat =
x => if(iszero x) then 1 elsex*f (pred x)
Page 20:
20 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
Syntax 𝜆◦
N
𝑛 ::= 0|1|··· Numeral Constants
𝑏 ::= true|false Boolean Constants
𝑇 ::=···| Nat|Bool Types
𝑡 ::=···| nat𝑛|succ𝑡|pred𝑡|mul𝑡𝑡|iszero𝑡
|bool𝑏|if𝑡then𝑡else𝑡 Terms
Γ ::=... Typing Environments
Term Typing Γ𝜑⊢𝑡:𝑄
Γ𝜑⊢𝑛:Nat∅(t-nat)
Γ𝜑⊢𝑡:Nat𝑝
Γ𝜑⊢succ𝑡:Nat𝑝(t-succ)
Γ𝜑⊢𝑡1:Nat𝑝Γ𝜑⊢𝑡2:Nat𝑞
Γ𝜑⊢mul𝑡1𝑡2:Nat𝑝,𝑞(t-mul)Γ𝜑⊢𝑡:Nat𝑝
Γ𝜑⊢iszero𝑡:Bool∅(t-iszero)
Γ𝜑⊢𝑡:Nat𝑝
Γ𝜑⊢pred𝑡:Nat𝑝(t-pred)
Γ𝜑⊢𝑏:Bool∅(t-bool)
Γ𝜑⊢𝑡1:Bool𝑝Γ𝜑⊢𝑡2:𝑇𝑞Γ𝜑⊢𝑡3:𝑇𝑟
Γ𝜑⊢if𝑡1then𝑡2else𝑡3:𝑇𝑞,𝑟(t-if)
Reduction Contexts, Values
𝐶::=□|succ𝐶|pred𝐶|mul𝐶𝑡|mul𝑡𝐶|iszero𝐶|if𝐶then𝑡else𝑡Reduction Contexts
𝑣::=nat𝑛|bool𝑏 Values
Reduction Rules 𝑡|𝜎→𝑡|𝜎
𝐶[succ nat𝑛]|𝜎→𝐶[nat(𝑛+1)]|𝜎 (succ)
𝐶[mul nat𝑛1nat𝑛2]|𝜎→𝐶[nat(𝑛1×𝑛2)]|𝜎 (mul)
𝐶[pred nat𝑛]|𝜎→𝐶[nat(max(0,𝑛−1))]|𝜎(pred)
𝐶[iszero nat𝑛]|𝜎→𝐶[bool(𝑛=0)]|𝜎 (iszero)
𝐶[if bool true then 𝑡1else𝑡2]|𝜎→𝐶[𝑡1]|𝜎 (if-true)
𝐶[if bool false then 𝑡1else𝑡2]|𝜎→𝐶[𝑡2]|𝜎 (if-false)
Fig. 9. Typing rules, reduction contexts, and reduction rules for natural numbers and boolean expressions
in𝜆◦<:.
valn : Nat = ...
fix[Nat](fact _fix)(n) // compute n!
Although in both case studies, we specialize the fixpoint operator with untracked types ( e.g.Unit
orNat), the system supports reachability polymorphism, allowing the fixpoint operator to be used
with more complex types , including closures. This extends its applicability beyond simple base
types to functions that capture references, enabling more advanced recursive computations.
All examples in this section are type-checked in Coq, and implemented in Scala.
5 Related Work
Reachability Types .RT provide a structured way to track ownership and aliasing in higher-
order programs, enabling precise reasoning about resource sharing and separation.
Page 21:
Complete the Cycle: Reachability Types with Expressive Cyclic References 21
The initial work on RT is presented in Bao et al .[2021], where tracked reachability sets enable
ownership-style reasoning for higher-order languages. They demonstrate the system’s ability to
integrate with a flow-sensitive effect system and express diverse programming patterns. Polymor-
phic Reachability Types [Wei et al .2024] enhance RT by introducing reachability polymorphism,
enabling more precise tracking of fresh resources and improving the expressiveness of ownership
reasoning in higher-order settings.
Based on Wei et al .[2024]’s polymorphic calculus, we introduce cyclic reference types, enabling
recursive constructs without built-in mechanisms. Our system extends non-cyclic references to
generalize the semantics introduced in Wei et al .[2024], providing additional flexibility for cyclic
structures. Unlike previous work which focused on non-cyclic reference tracking, our system
introduces cyclic reference types, enabling recursive constructs without modifying the core type
system. We also refine the reference introduction rule to increase precision and allow flexible graph
structures with nested references (see Section 2.4).
Following Dependent Object Types (DOT) [Amin et al .2016; Rompf and Amin 2016], RT functions
track their captured variables via self-references, ensuring precise tracking of shared resources. In
principle, function self-references could be used within the function body to encode non-terminating
recursions ( e.g.def f() = f() ), making recursion a built-in feature. Instead, we explicitly enable
cycles through store locations, allowing cyclic references to model recursion without having
recursion as a primitive mechanism.
Bao et al .[2023] formalize RT using logical relations to prove key properties, including termi-
nation even in the presence of higher-order state, which is a key premise for our work to build
on. Graph IR [Bračevac et al .2023] integrates RT to improve alias analysis and optimize impure
higher-order programs by tracking fine-grained dependencies with an effect system. Jia et al .[2024]
address key challenges in self-references within Rust-like systems by proposing an enhanced notion
of subtyping and developing a sound and decidable bidirectional typing algorithm for reachability
types.
Fixed-point Combinator .The origin of the fixed-point combinator can be traced to computabil-
ity theory [Rogers 1967; Sangiorgi 2009], which characterizes the computational power of recursive
functions. Bekić [1984] formalizes recursion using fixed-point constructions, demonstrating that
all definable operations arise as fixed points of monotonic functions.
Landin’s Knot [Landin 1964] encodes mutual recursion through self-application using mutable
reference cells, a concept that later influenced cyclic references in this work. Goldberg [2005]
generalizes Curry’s fixed-point combinator to handle variadic mutually-recursive functions. Kise-
lyov [2020] delves into the diverse manifestations and applications of fixed-point combinators in
computation. Their approach is particularly relevant to this work, as it provides a structured way
to express recursion through a store using cyclic references.
Our approach to cyclic references also draws inspiration from Landin’s Knot, and our case
studies further explore the deep connection between recursion and fixed-point constructs. While
Koronkevich and Bowman [2022] restricts non-termination in higher-order reference systems via
environment quantification, our work deliberately enables controlled non-termination, leveraging
cyclic references for recursion modeling.
Separation .Separation Logic [Reynolds 2002] provides a formal framework for local, spatial
reasoning about mutable heap structures, utilizing a separating conjunction operator to enforce
memory disjointness. RT [Bao et al .2021; Wei et al .2024] incorporates principles of Separation
Logic, particularly in its application type rule ( t-app-fresh ), where the overlap operator ensures
disjointness between function and argument qualifiers, maintaining separation guarantees in
type reasoning. In this work, we reuse [Wei et al .2024]’s notion of separation expressed by the
Page 22:
22 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
overlap operator (see Section 3) in t-app-fresh . Unlike previous approaches that rely on universally
quantified saturated upper bounds, we use an algorithmic transitive closure method to compute
qualifier overlap, yielding greater precision in qualifier reasoning (see Section 3.4).
Ensuring static separation is crucial for safe concurrent programming. Capture Separation
Calculus (CSC) [Xu et al .2023, 2024] extends Capture Calculus (CC) [Boruch-Gruszecki et al .
2023] to enforce static separation and data race freedom, ensuring non-interference of concurrently
executing threads. De Vilhena and Pottier [2021] extend separation logic with built-in effect handlers
to reason about cooperative concurrency and stateful computations, guaranteeing safe access to
heap-allocated mutable state.
Recursive Types and Existential Types .Alias Types [Smith et al .2000] extends linear types
with aliasing to enable efficient and safe memory management, leveraging existential types to
abstract specific memory locations. Walker and Morrisett [2000] employ existential types to capture
memory shape information, particularly focusing on the typing of recursive data structures through
parameterized recursive types that represent circular references. Ahmed et al .[2007] further utilize
existential types to abstract memory locations, whereas Grossman et al .[2002] employ them to
implement closures, where function pointers are paired with existentially quantified environments
to enforce region bounds and ensure region liveness.
In contrast, our approach introduces a “quasi-existential” qualifier with a semantics akin to that
of recursive self types in DOT [Amin et al .2016; Rompf and Amin 2016], where the identity of
the parent reference is retained. We deliberately avoid existential types in the context of cyclic
references, as they fail to preserve the identity of the cyclic reference, leading to a loss of precision.
For example, dereferencing (see Section 3.2.2) the same cyclic reference modeled by existential
types multiple times would produce values that appear separate, even though they originate from
the same reference.
Regions, Ownership, and Substructural Type Systems .Milano et al .[2022] introduce a system
to guarantee separation and safety in concurrent programs, combining linear typing, and region-
based memory management. However, while their work focuses on thread-level separation via
region types, RT address higher-order functions, providing fine-grained alias tracking at the level
of individual resources. Tofte and Talpin [1997] use regions to enforce sound life-time management,
proving semantic equivalence between source and target semantics, ensuring the absence of use-
after-free error. While their primary goal is a sound region inference algorithm for safe deallocation,
our work prioritizes soundness and separation, particularly in the presence of cyclic references
and recursive constructs. However, region-based guarantees such as deallocation safety can still be
achieved within RT by layering an effect system [Bao et al. 2021].
Haller and Odersky [2010] propose a capability-based system that enforces at-most-once con-
sumption of unique references while allowing flexible borrowing. Linear Haskell [Bernardy et al .
2018] extends Haskell’s type system with linear types, providing fine-grained control over resource
usage.
Capabilities and Path Dependent Types, and Qualified Types .Dependent Object Types
(DOT) [Rompf and Amin 2016] is formal model of a subset of the Scala type system with proven
soundness guarantee. One analogous feature of DOT with this work is that it uses term-level
recursive self types . DOT imposes restriction on dependent application, where arguments are
required to be of variable form, similar to t-sassgn-v in this work (see Sections 2.2 and 3.2).
However, recursive self types in DOT are used to access member types, while RT use the self-
referential variable in cyclic reference for qualifier tracking. Rapoport and Lhoták [2017] extend
DOT with mutable reference cells, proving the soundness of their system. However, their types
Page 23:
Complete the Cycle: Reachability Types with Expressive Cyclic References 23
remain unqualified, making it unsuitable for reachability tracking. Dort and Lhoták [2020] extend
Dependent Object Types (DOT) with reference mutability system to enable fine-grained access
control on references and provide immutability guarantees. Dort [2024] focuses on side effect free
(SEF) function types, ensuring function purity statically.
Capturing Types (CT) [Boruch-Gruszecki et al .2023] is a type system implemented in Scala,
designed to track captured capabilities. While CT makes use of boxing/unboxing operations, inspired
by contextual modal type theory (CMTT) [Nanevski et al .2008], RT’s use of the qmarker eliminates
the need of boxing and unboxing, allowing for finer-grained types that precisely model functions
returning fresh values.
Qualified types have been widely adopted to perform safety analysis such as const qualifier
inference in system-level languages [Foster et al .2006], reference immutability in Java [Huang et al .
2012], and polymorphic type systems supporting higher-order functions [Lee and Lhoták 2023].
6 Limitation and Future Work
This section outlines three categories of limitations in our work. First, we discuss the intrinsic
limitations ofour solution with respect to its goal of adding expressive cyclic references (Section 6.1).
Specifically, we prevent the formation of cyclic structures across multiple “hops”. Second, we
highlight limitations that our approach introduced on the base system (Section 6.2). We focus on
restrictions in deep substitution for function applications. While these constraints ensure soundness,
they limit expressiveness in certain cases. Finally, we examine limitations inherited from prior
work (Section 6.3). Particularly, the invariance of reference types restricts the ability of references
capturing local resources to escape their scope. While 𝜂-expansion offers a workaround, a more
refined subtyping mechanism for escaping self-references remains an open research challenge.
6.1 Limitations of Our Solution
One limitation of our solution is that it does not provide a way to construct deeply nested cyclic
references that contain multiple “hops” through the store. For example, consider the type
𝝁𝑧.Ref[𝝁𝑥.Ref[𝑇𝑧]]
Here, the inner referent’s qualifier refers to the qualifier for its outer parent z, rather than that
of its immediate parent x. This kind of multi-hop cycle is uninhabited in our system due to the
restricted introduction rule for cyclic reference types. Currently, our introduction rules ensure that
self-references must be directly tied to their immediate parent, preventing references from skipping
intermediate levels in the store.
The challenges involved in supporting deeply nested cyclic references include:
(1)Well-formed Condition and Type Soundness : Ensuring that a reference remains well-
typed across multiple levels of indirection is nontrivial. A reference must not inadvertently
escape its intended scope thus violating well-formedness and soundness.
(2)Qualifier Tracking Complexity : When allowing multi-hop cycles, the qualifier tracking
mechanism must correctly propagate reachability information across multiple levels. This
requires refinements in how qualifier inheritance and upcasting are handled.
(3)Assignment Semantics : Enabling assignments to deeply nested cyclic references requires
a precise formulation of how reference qualifiers are updated. Without strict control, such
assignments could lead to ambiguous or unsound behaviors.
Nevertheless, introducing a more expressive introduction form for cyclic reference that supports
this form of deeply nested cyclic references would further enhance the expressiveness of the system,
and we leave it as a future direction.
Page 24:
24 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
6.2 Limitations Introduced by Our Solution
A key limitation introduced by our approach is that deep substitution is no longer fully general
in non-fresh function applications ( i.e.t-app ). In prior formulations, deep substitution allowed a
function application to substitute its argument deeply within the function body without additional
constraints. However, in our system, this behavior is restricted unless the qualifier of the argument
is an optional singleton.
Specifically, when applying a function in a non-fresh context, we must enforce an additional
constraint: the function argument must not appear in the return type of the function. This restriction
is similar to the constraint already present in fresh function applications (see Section 3.2.4). The
rationale behind this limitation is to ensure consistent qualifier tracking and prevent unintended
aliasing, which could otherwise introduce unsound behaviors.
Despite this restriction, the practical impact on expressiveness is minimal. Similar to the Depen-
dent Object Types (DOT) system [Rompf and Amin 2016], this loss of precision does not significantly
hinder usability. In cases where deep substitution is blocked due to this limitation, a straightforward
workaround exists: one can introduce an intermediate variable to hold the function argument
and then use that variable in the function body to achieve deep substitution. This transformation
effectively preserves the intended behavior while maintaining the system’s type safety guarantees.
Therefore, while our approach imposes additional constraints on non-fresh function applications,
the practical impact is limited, as a simple variable introduction pattern can recover most of the
lost flexibility.
6.3 Inherent Limitations from Prior Work
Following Wei et al .[2024], reference types in our system are invariant. This invariance implies
that once a reference is assigned a qualifier, that qualifier cannot be relaxed or upcasted. A direct
consequence of this design is that a reference capturing a local resource cannot escape its original
scope, since its qualifier remains tied to the local environment. In contrast, a covariant or con-
travariant reference system might allow references to be generalized when escaping their defining
scope, but our system enforces strict qualifier tracking to maintain soundness.
One possible approach to support escaping references that capture local resources is to introduce
a subtyping rule for cyclic references. This rule would allow the inner qualifier to be moved to the
outer qualifier, effectively removing the inner qualifier’s local constraints. By doing so, references
that originally had local observability constraints could be reinterpreted in a broader context.
However, designing a sound and principled subtyping mechanism for self-referential references
introduces nontrivial challenges, particularly in ensuring that aliasing constraints and reachability
properties remain intact.
However, since subtyping of self references upon escape is an orthogonal problem, we leave it as
future work. In the meantime, when an escaping reference is required, we reuse the 𝜂-expansion
mechanism from Wei et al .[2024].𝜂-expansion allows a reference to be wrapped in an intermediate
function that reconstructs the original reference while modifying its qualifier. This technique
provides a sound and principled way to simulate reference escape, when subtyping rules for
escaping are not available.
7 Conclusion
In conclusion, this work presents a variant of the reachability types system that extends its reference
typing to allow cyclic references as well as precise, shallow referent qualifier tracking that enable
expressive programming patterns such as fixed-point combinators and non-terminating programs.
Page 25:
Complete the Cycle: Reachability Types with Expressive Cyclic References 25
Acknowledgments
References
Martín Abadi and Marcelo P. Fiore. 1996. Syntactic Considerations on Recursive Types. In Proceedings, 11th Annual IEEE
Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996 . IEEE Computer Society,
242–252.
Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L^3: A Linear Language with Locations. Fundamenta Informaticae
77, 4 (Jan. 2007), 397–449.
Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object
Types. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th
Birthday (Lecture Notes in Computer Science, Vol. 9600) , Sam Lindley, Conor McBride, Philip W. Trinder, and Donald
Sannella (Eds.). Springer, 249–272.
Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, and Tiark Rompf. 2021. Reachability Types: Tracking
Aliasing and Separation in Higher-Order Functional Programs. Proc. ACM Program. Lang. 5, OOPSLA (Oct. 2021),
139:1–139:32.
Yuyan Bao, Guannan Wei, Oliver Bračevac, and Tiark Rompf. 2023. Modeling Reachability Types with Logical Relations.
arXiv:2309.05885
Erik Barendsen and Sjaak Smetsers. 1996. Uniqueness Typing for Functional Languages with Graph Rewriting Semantics. 6,
6 (1996), 579–612.
Hans Bekić. 1984. Definable Operations in General Algebras, and the Theory of Automata and Flowcharts. In Programming
Languages and Their Definition: H. Bekič (1936–1982) , C. B. Jones (Ed.). Springer, Berlin, Heidelberg, 30–55.
Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. 2018. Linear
Haskell: Practical Linearity in a Higher-Order Polymorphic Language. Proc. ACM Program. Lang. 2, POPL (2018), 5:1–5:29.
Aleksander Boruch-Gruszecki, Martin Odersky, Edward Lee, Ondřej Lhoták, and Jonathan Brachthäuser. 2023. Capturing
Types. ACM Trans. Program. Lang. Syst. 45, 4 (Nov. 2023).
Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf. 2023. Graph
IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies.
Proc. ACM Program. Lang. 7, OOPSLA2 (Oct. 2023), 236:400–236:430.
Dave Clarke, Johan Östlund, Ilya Sergey, and Tobias Wrigstad. 2013. Ownership Types: A Survey. In Aliasing in Object-
Oriented Programming. Types, Analysis and Verification , Dave Clarke, James Noble, and Tobias Wrigstad (Eds.). Lecture
Notes in Computer Science, Vol. 7850. Springer, 15–58.
David G. Clarke, James Noble, and John M. Potter. 2001. Simple Ownership Types for Object Containment. In ECOOP 2001 —
Object-Oriented Programming , Jørgen Lindskov Knudsen (Ed.). Springer, Berlin, Heidelberg, 53–76.
David G. Clarke, John Potter, and James Noble. 1998. Ownership Types for Flexible Alias Protection. In Proceedings of
the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications, OOPSLA 1998,
Vancouver, British Columbia, Canada, October 18-22, 1998 , Bjørn N. Freeman-Benson and Craig Chambers (Eds.). ACM,
48–64.
Paulo Emílio De Vilhena and François Pottier. 2021. A Separation Logic for Effect Handlers. Proceedings of the ACM on
Programming Languages 5, POPL (Jan. 2021), 1–28.
Vlastimil Dort. 2024. Pure Methods for roDOT. (2024).
Vlastimil Dort and Ondřej Lhoták. 2020. Reference Mutability for DOT. In LIPIcs, Volume 166, ECOOP 2020 , Vol. 166. Schloss
Dagstuhl – Leibniz-Zentrum für Informatik, 18:1–18:28.
Jeffrey S. Foster, Robert Johnson, John Kodumal, and Alex Aiken. 2006. Flow-Insensitive Type Qualifiers. ACM Transactions
on Programming Languages and Systems 28, 6 (Nov. 2006), 1035–1087.
Jean-Yves Girard. 1987. Linear Logic. Theoretical Computer Science 50 (1987), 1–102.
Mayer Goldberg. 2005. A Variadic Extension of Curry’s Fixed-Point Combinator. Higher-Order and Symbolic Computation
18, 3 (Dec. 2005), 371–388.
Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. 2002. Region-Based Memory
Management in Cyclone. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and
Implementation (PLDI ’02) . Association for Computing Machinery, New York, NY, USA, 282–293.
Philipp Haller and Martin Odersky. 2010. Capabilities for Uniqueness and Borrowing. In ECOOP 2010 – Object-Oriented
Programming , Theo D’Hondt (Ed.). Springer, Berlin, Heidelberg, 354–378.
John Hogg. 1991. Islands: Aliasing Protection in Object-Oriented Languages. In Proceedings of the Sixth Annual Conference
on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA 1991, Phoenix, Arizona, USA, October
6-11, 1991 , Andreas Paepcke (Ed.). ACM, 271–285.
Wei Huang, Ana Milanova, Werner Dietl, and Michael D. Ernst. 2012. Reim & ReImInfer: Checking and Inference of
Reference Immutability and Method Purity. SIGPLAN Not. 47, 10 (Oct. 2012), 879–896.
Page 26:
26 Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, and Tiark Rompf. 2024. Escape with Your Self: A Solution to the Avoidance
Problem with Decidable Bidirectional Typing for Reachability Types. arXiv:2404.08217 [cs]
Oleg Kiselyov. 2020. Many Faces of the Fixed-Point Combinator. https://okmij.org/ftp/Computation/fixed-point-
combinators.html.
Paulette Koronkevich and William J Bowman. 2022. One Weird Trick to Untie Landin’s Knot. (2022).
P. J. Landin. 1964. The Mechanical Evaluation of Expressions. Comput. J. 6, 4 (Jan. 1964), 308–320.
Edward Lee and Ondřej Lhoták. 2023. Simple Reference Immutability for System F <:.Proceedings of the ACM on Programming
Languages 7, OOPSLA2 (Oct. 2023), 857–881.
Nicholas D. Matsakis and Felix S. Klock II. 2014. The Rust Language. In Proceedings of the 2014 ACM SIGAda Annual
Conference on High Integrity Language Technology, HILT 2014, Portland, Oregon, USA, October 18-21, 2014 , Michael B.
Feldman and S. Tucker Taft (Eds.). ACM, 103–104.
Mae Milano, Joshua Turcotti, and Andrew C. Myers. 2022. A Flexible Type System for Fearless Concurrency. In PLDI ’22:
43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA,
June 13 - 17, 2022 , Ranjit Jhala and Isil Dillig (Eds.). ACM, 458–473.
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual Modal Type Theory. ACM Transactions on
Computational Logic 9, 3 (2008), 23:1–23:49.
Benjamin C. Pierce. 2002. Types and Programming Languages . MIT Press.
Marianna Rapoport and Ondřej Lhoták. 2017. Mutable WadlerFest DOT. Proceedings of the 19th Workshop on Formal
Techniques for Java-like Programs (June 2017), 1–6.
John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symposium on Logic in
Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings . IEEE Computer Society, 55–74.
H. (Hartley) Rogers. 1967. Theory of Recursive Functions and Effective Computability . New York, McGraw-Hill.
Tiark Rompf and Nada Amin. 2016. Type Soundness for Dependent Object Types (DOT). SIGPLAN Not. 51, 10 (Oct. 2016),
624–641.
Davide Sangiorgi. 2009. On the Origins of Bisimulation and Coinduction. ACM Trans. Program. Lang. Syst. 31, 4 (2009),
15:1–15:41.
Frederick Smith, David Walker, and Greg Morrisett. 2000. Alias Types. In Programming Languages and Systems , Gert Smolka
(Ed.). Springer, Berlin, Heidelberg, 366–381.
Mads Tofte and Jean-Pierre Talpin. 1997. Region-Based Memory Management. Information and Computation 132, 2 (Feb.
1997), 109–176.
Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods: Proceedings of the IFIP
Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990 ,
Manfred Broy and Cliff B. Jones (Eds.). North-Holland, 561.
David Walker and J. Gregory Morrisett. 2000. Alias Types for Recursive Data Structures. In Types in Compilation (Lecture
Notes in Computer Science, Vol. 2071) . Springer, 177–206.
Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, and Tiark Rompf. 2024. Polymorphic Reachability Types: Tracking
Freshness, Aliasing, and Separation in Higher-Order Generic Programs. Proceedings of the ACM on Programming
Languages 8, POPL (Jan. 2024), 393–424.
Yichen Xu, Aleksander Boruch-Gruszecki, and Martin Odersky. 2023. Degrees of Separation: A Flexible Type System for
Data Race Prevention. IWACO (2023).
Yichen Xu, Aleksander Boruch-Gruszecki, and Martin Odersky. 2024. Degrees of Separation: A Flexible Type System for
Safe Concurrency. Proc. ACM Program. Lang. 8, OOPSLA1 (April 2024), 136:1181–136:1207.
