Escape with Your Self: Expressive Reachability Types with Sound and Decidable Bidirectional Type Checking

Songlin Jia

Purdue University
West Lafayette

Guannan Wei

Purdue University
West Lafayette

Siyuan He

Purdue University
West Lafayette

Yueyang Tang

Purdue University
West Lafayette

Yuyan Bao

Augusta University

Tiark Rompf

Purdue University

Despite Rust's success in systems programming, its “shared XOR mutable”
principle significantly restricts how mutable values can be used,
precluding many useful functional programming idioms.
Reachability types are a recent proposal to address the key limitations of
Rust-style “shared XOR mutable” approaches by tracking lifetimes and
reachability of shared, escaping, and mutable data, even in the presence of
higher-order functions and polymorphic types.
The key to enable such expressiveness is the notion of self-references in
reachability qualifiers.
However, self-references present major challenges in designing expressive
subtyping and decidable type checking algorithms, since self-references
are neither fully covariant nor fully contravariant, yet still need to
vary in certain circumstances.
Thus, making reachability types practical and bringing the benefits of
programming with lifetimes and sharing to higher-level
languages remains an open challenge.

In this paper, we investigate the issues of subtyping and type checking of
self-references for reachability types.
We address key gaps in previous work by presenting the
$\maybelang$-calculus of reachability types with a refined notion of
subtyping, which is more expressive compared to prior work, and
more smoothly supports features such as Church-encoded datatypes.
We also develop a sound and decidable bidirectional type checking algorithm,
which is implemented and verified in the Coq proof assistant.

<concept_desc>Software and its engineering Semantics</concept_desc>
<concept_desc>Software and its engineering Functional languages</concept_desc>
<concept_desc>Software and its engineering General programming languages</concept_desc>

[300]Software and its engineering Semantics
[500]Software and its engineering Functional languages
[500]Software and its engineering General programming languages

basewidth=0.56em, 0.52em,

§ INTRODUCTION

Mutable state with possible aliasing enables flexible and expressive programming
patterns, but is also non-trivial to reason about, thus leading to unsafe
programs, resource leaks, and even security issues.
For this reason, there has been a surge of interest in language
designs that regulate aliasing or mutability through a type system
Rust <cit.>, the most notable example, has shown that
lifetime tracking based on ownership types is an
eminently practical way of ensuring memory safety and other desirable
properties in a low-level imperative system language.
Although Rust's approach is practical and seeing widespread adoption,
it also remains fairly restrictive: its underlying “shared XOR mutable”
model severely constrains how mutable values can be used.
Specifically, any sharing of resources precludes mutation, preventing
programmers from using many common functional programming
idioms that are based on capturing and sharing mutable values
(see, , <Ref>).

Reachability types <cit.> are a recent proposal to address the key
limitations of Rust-style “shared XOR mutable” approaches, and
bring the benefits of programming with lifetimes and sharing to
higher-level languages.
The basic idea is to augment the type system with an additional qualifier
that tracks the reachable resources of an expression.
Instead of imposing global invariants on mutable references as in Rust,
reachability types track sharing and reachability information,
imposing restrictions such as uniqueness and separation at
a higher level.
Such a design overcomes the key limitation of Rust-style approaches,
and supports tracking lifetimes and reachability of
shared, escaping, and mutable data, even in the presence of higher-order
functions and polymorphic types.
However, while reachability types have shown great promise for
increased expressiveness, they have not so far been shown to be
truly practical: <cit.> have presented reachability type
systems in a declarative formulation along with mechanized proofs of soundness
and key memory invariants, but have left practical type checking
and inference algorithms as open challenges. Furthermore,
some gaps remain in understanding how to extend the core
calculi with richer language features such as algebraic data types.

Self-references for Tracking Escaped Data
The key ingredient that enables faithful tracking of escaping values is
the notion of self-references in reachability qualifiers, a concept
adopted from path-dependent types in DOT <cit.>.
In the core calculus of reachability types, self-references are identifiers attached to
functions, but can be generalized to other types, e.g., data structures.
When used in qualifiers, self-references serve as an upper bound on the reachability
of objects they attached to, thus providing a lightweight mechanism to
encapsulate reachability when dealing with escaping.
For example, $f$ is the self-reference for function type $f(x: T_1) \to T_2$,
and $f$ over-approximates the free variables observed by the function.

def counter(n: Int) =              // counter: Int => $\mu$p.Pair[(()=>Unit)$\trackvar{p}$, (()=>Unit)$\trackvar{p}$]$\trackfresh$
val c = ref n                     //  : Ref[Int]$\trackvar{c}$
(() => c += 1, () => c -= 1)      //  : Pair[(()=>Unit)$\trackvar{c}$, (()=>Unit)$\trackvar{c}$]$\trackvar{c}$

// instantiate the self-reference $\mathtt{p}$ with bound name $\mathtt{ctr}$:
val ctr = counter(0)                //  : Pair[(()=>Unit)$\trackvar{ctr}$, (()=>Unit)$\trackvar{ctr}$]$\trackvar{ctr}$
// name $\mathtt{ctr}$ abstracts over its captured variables:
val incr = fst(ctr)                 //  : (()=>Unit)$\trackvar{ctr}$
val decr = snd(ctr)                 //  : (()=>Unit)$\trackvar{ctr}$

Expressiveness gains of reachability types over Rust
for common FP idioms
(example from <cit.>):
self references in the types of escaping values such as
$\mu p. \text{Pair}[A^p,B^p]$ enable safe sharing of mutable values.
The example is not typeable in safe Rust, due to Rust's
“shared XOR mutable” policy.

Using a concrete example, <Ref> illustrates the use of
self-references to track shared, escaping, and mutable data.
The function @counter@ returns a pair of functions, which both capture
the same locally defined mutable reference<EMAIL_ADDRESS>Once leaving the defining
scope of @c@, we do not have a direct, nominal way to refer to
the underlying mutable resource.
To properly maintain the sharing invariant between the two returned functions
after escaping, reachability types assign a self-reference $p$ to the pair
object, which is then referenced by the two returned functions, indicating that
these two functions reach some shared resource hidden under $p$.
Once the returned value is bound to another variable @ctr@, we can
instantiate the self-reference to<EMAIL_ADDRESS>The projected components from the pair both reach @ctr@, thus the
sharing invariant is properly maintained after escaping.

Challenges of Adopting Self-references
Unfortunately but not surprisingly, self-references are also the biggest source
of trouble for (1) designing a subtyping relation that is sound and expressive
and (2) a type checking/inference algorithm that is sound and decidable.
These challenges impair the practical adoption of reachability types.
The key reason is that self-references are neither fully covariant nor fully
contravariant (see discussion in <Ref>), but still need to vary in
certain circumstances to be useful.
When used in practice, for example, to type check the @counter@ function in
<Ref> involving escaping data structures,
prior work by <cit.> requires a term-level coercion to
re-type a term, where a more natural way would be to “upcast” the qualifier to
self-references using the subtyping relation.
Extending subtyping for expressiveness but without special care for
self-references can lead to unsoundness in terms of tracking reachability.

When it comes to a practical implementation, although bidirectional typing
<cit.> is well-developed for the
underlying substrate of
reachability types (i.e., System $F_{<:}$), a type checking algorithm
still has to decide a subtyping relation involving self-references.
It is also desirable for the inference algorithm to infer when a type should be
upcast to subsuming self-references, which is necessary to avoid deducing
ill-scoped qualifiers.
A similar and longstanding issue has been identified as the avoidance problem
in the context of ML-style module systems <cit.>.

Refined Calculus with Expressive Subtyping
We first develop a refined $\maybelang$-calculus for reachability types
based on the key observation that subtyping involving self-references is
meaningful only with respect to the observable locations of the corresponding
Thus, subtyping rules for types and qualifiers need to be combined.
By providing multiple rules for self-references in different positions, along
with the new concept of qualifier growth (see <Ref>), the
refined calculus is made sound and expressive.  The calculus also adapts
function application rules to fit with the semantics of self-references and to
make it more amenable for type checking.

Bidirectional Type-and-Qualifier Checking
After presenting the declarative rules of the refined calculus,
we develop a corresponding bidirectional typing algorithm in three steps.
First, the qualifier subsumption algorithm unfolds qualifiers along
dependencies. Second, the subtyping algorithm checks type subsumption,
connecting multiple subtyping rules if necessary. Third, at the top level, the
bidirectional typing algorithm switches among three checking/inference modes,
including one hybrid
mode to check against an expected type while synthesizing a qualifier.
While our calculus does not include quantified type abstraction,
this hybrid mode enables a lightweight form of qualifier polymorphism
through dependent application.
We further present the soundness and decidability results of our algorithm with
mechanized proofs.

Data Structure Encodings

We investigate the expressiveness of our systems by discussing
Church-encoded data types. On the one hand, these are indispensable tools
in everyday programming, and thus their encodings justify adding
corresponding primitives to the language.
On the other hand, the data structure encodings themselves are higher-order
programs, which serve as a validation of the expressiveness and effectiveness
of our type checking algorithm.
We present a case study on Church-pairs, discussing their
usages, subtyping derivations, and annotation requirements.

Contributions and Organization
In this work, we address key gaps in previous developments on reachability types
<cit.> by (1)
designing the $\maybelang$-calculus with a refined notion of subtyping,
and (2) developing a sound and decidable bidirectional type checking
algorithm, implemented and verified in Coq.
Our subtyping relation and type checking algorithm lead to smoother support for a
variety of high-level constructs used in practice (such as pairs in

* We introduce the basic mechanism of reachability types, and
identify the key challenges in realizing effective type checking/inference
procedures related to self-references (<Ref>). We discuss
soundness pitfalls in naively extending the subtyping relation for

* To soundly improve the expressiveness of the subtyping relation,
we present the $\maybelang$-calculus with key changes in subtyping (<Ref>).
The refined subtyping rules allow flexible dependencies to arguments and
self-references in both covariant and contravariant positions.

* We present a bidirectional typing algorithm for our calculus with
proofs of soundness and decidability (<Ref>).
The algorithm is deterministic and includes a hybrid mode combining
type checking and qualifier inference.

* We present a case study on the Church-encoding of data structures
In contrast to prior work <cit.>, the
refined calculus does not require term-level coercions to handle escaping
data, demonstrating its improvement in expressiveness.

* We further discuss an extension of the calculus with flow-sensitive effects
and its effect checking/inference algorithm (<Ref>).
The effect system enables move semantics and compiler optimizations in
imperative higher-order languages.

We discuss related work in <Ref> and conclude the paper
with <Ref>.

§ MOTIVATION

In this section, we first informally introduce the key mechanics of reachability
types based on <cit.>'s formalization $\popllang$.
We then discuss how to address the limitations on self-references in $\popllang$ and
motivate the design of $\maybelang$ in <Ref>.
We further
discuss the challenges in putting $\maybelang$
into practice via bidirectional typing in <Ref>.

§.§ Reachability Types in a Nutshell

§.§.§ Qualifiers and Freshness

Reachability types track the reachable definitions of expressions via type qualifiers.
Shown below, the variable @n@ can be typed with its own name @n@ as the qualifier once defined.
Semantically, a qualifier denotes a set of memory locations reachable from
the value, and subtyping states that locations on the left are bounded
by the right hand side.
As integer values are primitive, the qualifier @n@
can eventually be “widened” to the empty set $\varnothing$ by looking at the context:

val n = 1; n               // [ n: Int$\track$ ] $\vdash$ Int$\trackvar{n}$ <: Int$\track$

To track memory references,
<cit.> introduce the freshness marker $\qfresh$ for
fresh allocations that are not (yet) associated with a name.
Shown below is a fresh reference marked with $\qfresh$ that is then bound to name<EMAIL_ADDRESS>Unlike integers, however, the name @m@ cannot be detached from the qualifier,
so as not to conflate @m@ for multiple separate values, since each fresh value
is considered distinct.

val m = ref n; m           // [ ..., m: Ref[Int]$\trackvar{\qfresh n}$ ] $\vdash$ Ref[Int]$\trackvar{m}$ $\not$<: Ref[Int]$n$
\end{lstlisting}
When leaving the scope of @m@, we do have to remove @m@
from the qualifier for well-scopedness. This is called \emph{avoidance} and obtained
by substituting @m@ with $$@n@ (cf. \Cref{sec:funcs}) in the
reachability qualifier, assuming @n@ remains in scope.
Thus, escaping can make a non-fresh value fresh again:
\begin{lstlisting}
{ val m = ref n; m }       // Ref[Int]$\trackvar{\qfresh n}$ = (Ref[Int]$\trackvar{m}$)[m $\mapsto$ $\qfresh$n]
\end{lstlisting}
However, it is important to note that substitution is no longer sound
once the escaping data is captured in a larger construct.
Consider returning a pair @(m<EMAIL_ADDRESS>If we substitute
the qualifier @m@ in both components when escaping, extracting the components
later yields two distinct fresh references sharing the \emph{same} actual value @m@,
which is unsound:
\begin{lstlisting}
val p = { val m = ref n; (m, m) }  // p: Pair[Ref[Int]$\trackvar{\qfresh n}$, Ref[Int]$\trackvar{\qfresh n}$]$\trackvar{\qfresh n}$
val m1 = fst(p)                    // m1: Ref[Int]$\trackvar{\qfresh n}$ $\leftarrow$ $\color{red}{\texttt{Unsound}}$
val m2 = snd(p)                    // m2: Ref[Int]$\trackvar{\qfresh n}$ $\leftarrow$ $\color{red}{\texttt{Unsound}}$
\end{lstlisting}
Reachability types address this issue by introducing a \emph{self-reference} for
the returned pair, so that the components can refer to the containing object.
Once assigning the pair to a variable, extracted components refer to that
assigned variable, thus the sharing invariant is maintained.
\begin{lstlisting}
val p = { val m = ref n; (m, m) }  // p: $\mu$p. Pair[Ref[Int]$\trackvar{p}$, Ref[Int]$\trackvar{p}$]$\trackvar{\qfresh n}$
val m1 = fst(p)                    // m1: Ref[Int]$\trackvar{p}$
val m2 = snd(p)                    // m2: Ref[Int]$\trackvar{p}$
\end{lstlisting}
In the spirit of a core calculus, we seek to \emph{encode} features such as
@let@-bindings and pairs in terms of functions (cf. \Cref{sec:encode}).
Hence, we need to understand the typing of functions next.

\subsubsection{Aliasing and Separation in Functions} \label{sec:funcs}
Modular reasoning about aliasing is enabled via function types.
As exemplified below, the function @falias@ observes the free variable @l@,
thus carrying @l@ in its qualifier. With the formal argument @x@ qualified by
@{m,l}@, the actual argument can alias to at most @m@ and<EMAIL_ADDRESS>Reachability types features a lightweight form of reachability polymorphism via
\emph{dependent application}. For example, the return type of @falias@ is
qualified by @x@, which will be substituted with the actual argument qualifier
when applied.
\begin{lstlisting}
val l = ref 0
def falias(x: Ref[Int]$\trackvar{m,l}$) =    // falias: ((x: Ref[Int]$\trackvar{m,l}$) => Ref[Int]$\trackvar{x}$)$\trackvar{l}$
{ x := !l; x }
falias(l)                    // Ref[Int]$\trackvar{l}$ = (Ref[Int]$\trackvar{x}$)[x $\mapsto$ l]
falias(m)                    // Ref[Int]$\trackvar{m}$ = (Ref[Int]$\trackvar{x}$)[x $\mapsto$ m]
falias(ref 0)                // Error: $\qfresh$ $\not$<: m,l
\end{lstlisting}

To enforce separation, the freshness marker $\qfresh$ has a \emph{contextual}
meaning when used in function argument qualifiers:
these functions can only accept arguments that are not already observed by the function
(i.e., arguments are separate from the function).
Thus, function @fsepa@ below cannot be applied to @l@, as @l@ is neither
permitted by @m@ nor separate from<EMAIL_ADDRESS>On the other hand, application to~@m@
or to a fresh reference is allowed.
\begin{lstlisting}
def fsepa(x: Ref[Int]$\trackvar{\QFresh m}$) =    // fsepa: ((x: Ref[Int]$\trackvar{\QFresh m}$) => Ref[Int]$\trackvar{x}$)$\trackvar{l}$
x := !l; x
fsepa(l)                    // Error: since l is observed by the function, thus not fresh
fsepa(m)                    // Ref[Int]$\trackvar{m}$ = (Ref[Int]$\trackvar{x}$)[x $\mapsto$ m]
fsepa(ref 0)                // Ref[Int]$\trackvar{\QFresh}$ = (Ref[Int]$\trackvar{x}$)[x $\mapsto \QFresh$]
\end{lstlisting}

References to the formal parameter can be deeply nested inside the return type,
not just in the outermost qualifier, allowing to express \emph{deep dependency}
in higher-order programs.
Shown in the @fdeep@ function, at the time of application, all
occurrences of @x@ are replaced with the actual argument qualifier @m@:
\begin{lstlisting}
def fdeep(x: Ref[Int]$^\QFresh$) =     // fdeep: ((x: Ref[Int]$^\QFresh$) => $\textit{<type of inner>}$)$^\varnothing$
def inner(y: Ref[Int]$^\QFresh$) =   // inner: ((y: Ref[Int]$^\QFresh$) => Ref[Int]$\trackvar{x}$)$\trackvar{x}$
x := !y; x
fdeep(m)                     // ((y: Ref[Int]$^\QFresh$) => Ref[Int]$\trackvar{m}$)$\trackvar{m}$ = $\textit{<type of inner>}$[x $\mapsto$ m]
\end{lstlisting}

\vspace{-1ex}
\subsection{Typing and Subtyping Self-References} \label{sec:selfref}
\vspace{-.5ex}

The usage of self-references can be motivated from typing a variant of the
above @fdeep@ function: what if we want to apply @fdeep@ to a fresh allocation?
At the first glance, this seems possible, since the argument is indeed
separate from the function:
However, the result type of the application leads to unsoundness:
\begin{lstlisting}
val cl = fdeep(ref 0)        // cl: ((y: Ref[Int]$^\QFresh$) => Ref[Int]$^\QFresh$)$^\QFresh$ = $\textit{<type of inner>}\;[x \mapsto \qfresh]$
cl(m)                        // Unsound: Ref[Int]$^\QFresh$
\end{lstlisting}
By dependent application, the type of result @cl@ carries two additional
freshness markers.
Since $\qfresh$ is always separate from $\qfresh$, applying @cl@ multiple times
yields distinct fresh results. Unfortunately, this behavior is unsound, since
in fact @cl@ always returns the same underlying resource.

To soundly permit this application, we need to type @fdeep@ alternatively with
Borrowed from Dependent Object Types (DOT)~\cite{DBLP:conf/birthday/AminGORS16},
self-references provides an identifier that can be referred by the subcomponents
of an object.
Here we present @fdeep@ again with self-reference types.
The return type of @inner@ is now qualified by @inner@ itself, and
the chain of aliasing is preserved through mapping @inner@ to the closure<EMAIL_ADDRESS>\begin{lstlisting}
def fdeep(x: Ref[Int]$^\QFresh$) =     // fdeep: ((x: Ref[Int]$^\QFresh$) => $\textit{<type of inner>}$)$^\varnothing$
def inner(y: Ref[Int]$^\QFresh$) =   // inner: ((y: Ref[Int]$^\QFresh$) => Ref[Int]$\trackvar{inner}$)$\trackvar{x}$
x := !y; x
// cl: ((y: Ref[Int]$^\QFresh$) => Ref[Int]$\trackvar{cl}$)$^\QFresh$ = $\textit{<type of inner>}$[x $\mapsto \QFresh$, inner $\mapsto$ cl]
val cl = fdeep(ref 0)        // cl: ((y: Ref[Int]$^\QFresh$) => Ref[Int]$\trackvar{cl}$)$^\QFresh$
cl(m)                        // Ref[Int]$\trackvar{cl}$
\end{lstlisting}

While typing with self-references enables soundly tracking
escaping closures with fresh resources, it is neither natural for inference,
nor as precise as typing with deep dependency for non-fresh cases.
To enjoy the best of both worlds, %
we need to connect the two type signatures of @fdeep@ via subtyping.
However, this is non-trivial and was left as an open challenge by \citet{DBLP:journals/pacmpl/WeiBJBR24}.
In essence, self-references are both lower bounded and upper bounded, but
neither covariant nor contravariant.
Now we present examples to motivate our formal development in \Cref{sec:subtyping}.

\newtheorem{lesson}{Lesson}

\subsubsection{Connecting Types and Qualifiers}

To enable subtyping between the two @fdeep@ signatures, we need
the following relation, where @inner@ is added in the typing
context, with @x@ in its observation,
\vspace{-1ex}
\infax{\ldots, x: \ty[\qfresh]{\textsf{Ref}}, \mathit{inner}: \ty[x]{(\cdots)}, \ldots \ts x <: \mathit{inner}}
\vspace{-1ex}
However, \citet{DBLP:journals/pacmpl/WeiBJBR24} have separate subtyping relations
for types and for qualifiers.
Following their subtyping derivation produces the following goal,
\vspace{-1ex}
\infax{\ldots, x: \ty[\qfresh]{\textsf{Ref}}, \mathit{inner}: \ty[\qfresh]{(\cdots)},\ldots \ts x <: \mathit{inner}}
\vspace{-1ex}
Overlooking the fact that types and qualified types occur in a nested
manner, the information on @inner@'s qualifier is lost, and thus
there is no way to state the bound conditions of<EMAIL_ADDRESS>In this way, the self-reference must stay invariant,
effectively preventing \citet{DBLP:journals/pacmpl/WeiBJBR24} from
discharging this goal.
As a result, they can only support escaping closures by
$\eta$-expansions that re-type the term.

\begin{lesson} \label{lsn:combine}
To enable subtyping with self-references, the type system must include
combined subtyping rules for types and qualifiers.
\end{lesson}

\subsubsection{Upper Bound Meets Lower Bound} \label{sec2:bounds}
Combining subtyping for types and qualifiers is not naively sound.
By the semantics that qualifiers are upper bounds on observations,
they should always be covariant with types (\textsc{sq-qual'}). On the other hand, to enable
avoiding a variable with the self-reference, the function observation should be
the lower bound of the self-reference (\textsc{q-self'}), as in the case of<EMAIL_ADDRESS>
\begin{minipage}{.4\linewidth}
\infrule[sq-qual']{\G\ts p <: q}{\G\ts \ty[p]{T} <: \ty[q]{T}}
\end{minipage}
\begin{minipage}{.4\linewidth}
\infrule[q-self']{f: \ty[q]{F}\in\G}{\G\ts q <: f}
\end{minipage}

Unfortunately, combining the two rules together leads to unsoundness.
Shown below, if the self-reference @fneg@ is attached on the argument, by
\textsc{\small{(q-self')}} the actual argument can be anything within @fneg@'s
observation (i.e., @m@).
\begin{lstlisting}
def fneg(x: Ref[Int]$\trackvar{fneg}$) = !x + !m // fneg: ((x: Ref[Int]$\trackvar{fneg}$) => Int$^\qbot$)$\trackvar{m}$
fneg(m)                            // m <: fneg
fneg(l)                            // Error: l $\not$<: fneg
\end{lstlisting}
We can then reassign @fneg@ to @fneg2@ while upcasting its qualifier via
\textsc{(sq-qual')}\footnote{The types of \texttt{fneg} and \texttt{fneg2} are
the same modulo $\alpha$-renaming on the self-reference.}.
Accidentally, this also allows applying @fneg2@ to @l@, breaking the
aliasing guarantee provided by<EMAIL_ADDRESS>%
\begin{lstlisting}
val fneg2: ((x: Ref[Int]$\trackvar{fneg2}$) => Int$^\varnothing$)$\trackvar{m,l}$ = fneg
fneg2(l)                   // l <: fneg2
\end{lstlisting}

\begin{lesson} \label{lsn:negative}
We should not interpret self-references in negative
positions as upper bounds.%
\end{lesson}

Nevertheless, the @farbi@ function below differs from @fneg@ only by attaching
the freshness marker on<EMAIL_ADDRESS>As the self-reference permits anything within the observation, and $\QFresh$
permits anything beyond, @farbi@ can take arbitrary arguments!
In this regard, expanding the observation of @farbi@ is still safe.
\begin{lstlisting}
def farbi(x: Ref[Int]$\trackvar{\qfresh farbi}$) = !x + !m // farbi: ((x: Ref[Int]$\trackvar{\qfresh farbi}$) => Int$^\qbot$)$\trackvar{m}$
farbi(l)                              // okay, since l is separate from farbi
val farbi2: ((x: Ref[Int]$^\textit{farbi2}$) => Int$^\varnothing$)$^{m,l}$ = farbi
farbi2(l)                             // okay, since l <: farbi2
\end{lstlisting}

\begin{lesson} \label{lsn:arbitrary}
A function with both freshness and the self-reference in the argument
qualifier should be able to take arbitrary arguments.
\end{lesson}

\subsubsection{Growing the Qualifier of a Function} \label{sec2:growth}
Self-references can help to avoid mentioning a variable from the function's
observation in the qualifier.
As observations are expandable by \textsc{(sq-qual')}, self-references can cover
more than that.
Consider the following example, where the function @fpos@
returns its argument<EMAIL_ADDRESS>\begin{lstlisting}
def fpos(x: Ref[Int]$\trackvar{m}$) = x := 0; x // fpos: ((x: Ref[Int]$\trackvar{m}$) => Ref[Int]$\trackvar{x}$)$^\varnothing$
fpos(m)                            // Ref[Int]$\trackvar{m}$ = (Ref[Int]$\trackvar{x}$)[x $\mapsto$ m]
\end{lstlisting}
Although @fpos@ is a closed function, it returns a piece of data @x@ that is
potentially aliased to @m@, even thought @fpos@ does not directly capture<EMAIL_ADDRESS>We can upcast the return qualifier to the self-reference, and \emph{at the same time}
widen the observation of the function to include @m@, as shown
by the typing ascription<EMAIL_ADDRESS>Then, applying @fpos2@ preserves the result reachability of @m@: %
\begin{lstlisting}
val fpos2: ((x: Ref[Int]$\trackvar{m}$) => Ref[Int]$\trackvar{fpos2}$)$\trackvar{m}$ = fpos
fpos2(m)                           // Ref[Int]$\trackvar{fpos2}$ <: Ref[Int]$\trackvar{m}$
\end{lstlisting}
Note that such a type change can be unsound if without including @m@ in the
function's qualifier.
We introduce the concept of \emph{growth} to note such behaviors
in enlarging the qualifier to include potential reachability (see \Cref{sec:subtyping}).
This again confirms Lesson \ref{lsn:combine} that types and qualifiers are
associated, where growth is the bridge.

\begin{lesson} \label{lsn:growth}
A change in the type can require a corresponding
change (growth) in the qualifier.
\end{lesson}

\subsubsection{Depending on the Growth} \label{sec2:depgrowth}

Although the notion of growth seems natural and benign on its own, its interaction
with other features could introduce unsoundness if not handled carefully.
To exemplify, we define a higher-order function @fdepgr@, whose result depends on
@f@ and the application result of @f@, which is a potential source of growth.
Applying @fdepgr@ to @fpos2@ defined earlier produces the resulting
reachability @fpos2@, which can be upcast to<EMAIL_ADDRESS>\begin{lstlisting}
// fdepgr: (f: ((x: Ref[Int]$\trackvar{m}$) => Ref[Int]$\trackvar{f}$)$\trackvar{m}$ => Ref[Int]$\trackvar{f}$)$\trackvar{m}$
def fdepgr(f: ((x: Ref[Int]$\trackvar{m}$) => Ref[Int]$\trackvar{f}$)$\trackvar{m}$) =
f(m)         // Ref[Int]$\trackvar{f}$
fdepgr(fpos2)  // Ref[Int]$\trackvar{fpos2}$ = (Ref[Int]$\trackvar{f}$)[f $\mapsto$ fpos2] <: Ref[Int]$\trackvar{m}$
\end{lstlisting}
Since argument types are \emph{contravariant}, we can cast @fdepgr@ to @fdepgr2@
by narrowing the argument type for @f@ (i.e. from the type of @fpos2@ to
@fpos@, both defined in the previous section).
However, then applying it to @fpos@ produces a reference with the empty qualifier!
Now, a resource that is supposed to be tracked becomes untracked, undermining the
soundness promise of the system.
\begin{lstlisting}
val fdepgr2: (f: ((x: Ref[Int]$\trackvar{m}$) => Ref[Int]$\trackvar{x}$)$^\varnothing$ => Ref[Int]$\trackvar{f}$)$\trackvar{m}$ = fdepgr
fdepgr2(fpos)  // Ref[Int]$\trackvar{fpos}$ = (Ref[Int]$\trackvar{f}$)[f $\mapsto$ fpos] <: Ref[Int]$^\varnothing$
\end{lstlisting}

\begin{lesson} \label{lsn:depgr}
Using qualifier growth in contravariant positions with dependent application
can produce a result qualifier smaller than expected, inducing unsoundness.
\end{lesson}

\paragraph{Summary}
Through concrete examples, sound and expressive treatment of
self-references requires the concept of \emph{growth} and position-aware
subtyping theories. We use these lessons to guide the design of $\maybelang$
subtyping in \Cref{sec:subtyping}.

\subsection{Challenges for Bidirectional Typing} \label{sec:challenge}

In addition to declaratively \emph{specifying} a more expressive notion
of subtyping for reachability types, we are also interested in the algorithmic
\emph{checking and inference} of types, a challenge left aside
by prior work~\cite{DBLP:journals/pacmpl/WeiBJBR24,DBLP:journals/pacmpl/BaoWBJHR21}.
Bidirectional typing~\cite{DBLP:journals/csur/DunfieldK21} offers well-studied
framework for this purpose.
However, adapting a non-trivial calculus such as $\maybelang$ requires work
beyond off-the-shelf recipes. Here, we identify the major challenges,
and present our bidirectional typing algorithm for $\maybelang$
in \Cref{sec:algo}.

\paragraph{Subtype Checking} While bidirectional typing provides straightforward
recipes for adapting typing rules, subtyping rules need to be considered
individually for each type system. While usually such rules are syntax-directed
and easy to adapt, this is not the case for reachability types.
Firstly, deciding the subsumption of qualifiers (or \emph{sub-qualifying}) is not
syntax-directed. Furthermore, the subtyping rules of $\maybelang$ are
complicated by self-references. Both parts rely heavily on transitivity
to connect multiple rules for rich behavior. Thus, a sound and decidable
adaption of~$\maybelang$ subtyping is critical but non-trivial.

\paragraph{Avoidance}
The precise type/qualifier of a function may not always be permissible for an
application (recall @fdeep@ on fresh references), and thus we need to adapt the
function type with self-references to avoid ill-scoped qualifiers.
Concretely, we need to find a supertype to avoid mentioning a variable from
deep inside, hence the \emph{avoidance} issue.
This is similar to subtype checking, with the right-hand side left open except
for the avoidance constraint.  Similar mechanisms have been studied in ML-style
module systems \cite{DBLP:journals/tcs/GhelliP98,lillibridgeTranslucentSumsFoundation,
DBLP:journals/jfp/Crary20, 10.5555/1087953}
and languages that feature weaker form of dependent types (e.g. path-dependent types in Scala).

\paragraph{Middle Ground between Checking and Inference} Pure checking or
inference is not always desirable for reachability types. For instance, the use
of dependent application requires an exact argument type but expects a finer
qualifier, so that more precise reachability can be obtained by substitution on
Supporting precise dependent application requires a hybrid mode to check the
type and synthesize the qualifier at the same time, which further requires the
subtype checking algorithm to synthesize a qualifier (or growth).

\section{Language Design} \label{sec:lang}

Here we present the formal theory and metatheory of $\maybelang$,
the core calculus
designed to explore sound and expressive subtyping of reachability types
based on $\popllang$ from \citet{DBLP:journals/pacmpl/WeiBJBR24}.
It features \textit{growth} to restore
the connection between types and qualifiers and position-aware rules for
soundness. The calculus and its metatheory have been fully mechanized in Coq.%
\footnote{\artifact}

\subsection{Syntax}

\begin{figure}[t]
\begin{mdframed}
\small
\judgement{Syntax}{\BOX{\maybelang}}\vspace{-7pt}
x,y,z   &\in & \Var                                                                            & \text{Variables} \\
f,g,h   &\in & \Var                                                                            & \text{Function Variables} \\
t       &::= & c \mid x \mid \lambda f(x).t \mid t~t \mid \tref~t \mid\ !~t \mid t \coloneqq t \mid \colorbox{lightgray}{\ensuremath{t: Q}} & \text{Terms}\\[1ex]
p,q,r   &\in & \mathcal{P}_{\mathsf{fin}}(\Var \uplus \{ \QFresh \})                           & \text{Reachability Qualifiers} \\
S,T,U,V &::= & B \mid f(x: \ty{Q}) \to \ty{Q} \mid \TRef~B                                     & \text{Base/Function/Reference Types} \\
O,P,Q,R &::= & \ty[q]{T}                                                                       & \text{Qualified Types} \\[1ex]
\flt,\colorbox{lightgray}{\ensuremath{\delta}} &\in & \mathcal{P}_{\mathsf{fin}}(\Var)         & \text{Observations/Growth} \\
\colorbox{lightgray}{\ensuremath{m}}    &\in & \mathcal{P}_{\mathsf{fin}}(\{ \QFresh, f, x \}) & \text{Dependent Variable Masks} \\
\Gamma  &::= & \varnothing\mid \Gamma, x : Q                                                   & \text{Typing Environments} \\
\end{array}$$\\
\textbf{\textsf{Qualifier Shorthands}} \qquad
p,q := p \qlub q\qquad x := \{x\} \qquad \QFresh :=\{\QFresh\}\qquad \starred{q} := \{\qfresh\}\qlub q \\
p \subq_m q := p\cap m \subq q\cap m \qquad p_{\setminus q} := p\setminus q
\end{array}$
\end{mdframed}
\caption{Syntax definitions of $\maybelang$ with qualifier shorthands for
compact presentation. Taken and adapted from \citet{DBLP:journals/pacmpl/WeiBJBR24},
with additions to their $\popllang$ \colorbox{lightgray}{shaded}.} \label{fig:terms}
\vspace{-2ex}
\end{figure}
\Cref{fig:terms} presents the syntax of $\maybelang$.
The calculus is built atop the simply-typed
$\lambda$-calculus with references and subtyping. We detail our extension with
qualifiers and our notations as follows.

Terms include constants, variables, function abstraction and application, and
reference operations. For illustration purposes, we use different metavariables
for ordinary variables (\ie $x,y,z$) and functions (\ie $f,g,h$). For the
abstraction term $\lambda f(x). t$ we add the self-reference $f$ allowing
the function type to refer to its own closure. We further add the ascription
term $t: Q$ for deriving bidirectional typing algorithm in \Cref{sec:algo}.

Qualified types ($Q$) are types ($T$) associated with a qualifier ($q$). Types
include base
types, function types, and reference types. For functions, the domain and
codomain are both qualified types, and their qualifiers can include dependent
references to the argument $x$ or the function $f$.
For references, we consider only those over
base types. Qualifiers are sets of variables with optionally
the freshness marker $\QFresh$, denoting a fresh value with no name, as
showcased in \Cref{sec:nutshell}.

In typing judgements, we use $\G$ for the typing context, and $\flt$ for the filter
to constrain the observation of the context. Being able to limit the
observation is a key device used to enforce separation in the mechanization.
Additionally, we use the metavariable $\delta$ to denote growth and $m$ to denote
dependent variable masks (\eg $\qfresh, x, f$). Both are slices of qualifiers
used for the subtyping judgements in \Cref{sec:subtyping}.

\begin{figure}[t]
\begin{mdframed}\small
\judgement{Qualifier Substitution}{\BOX{q[p/x]}\ \BOX{q[p/\qfresh]}\ \BOX{q[p/m]}}
\begin{array}{l@{\;}c@{\;}ll@{\quad\qquad\qquad\qquad}l@{\;}c@{\;}ll}
q[p/x]       &=& q\setminus\{x\}\qlub p & x\in q       & q[p/x]       &=& q & x\notin q  \\
q[p/\qfresh] &=& q\qlub p               & \qfresh\in q & q[p/\qfresh] &=& q & \qfresh\notin q \\
q[p/x,m]     &=& q[p/x][p/m]            &              & q[p/\qbot]   &=& q
\end{array}$$
\judgement{Reachability and Overlap}{\BOX{{\color{gray}\G\vdash}\,x \reaches x}\ \BOX{{\color{gray}\G\vdash}\, \qsat{q}}\ \BOX{{\color{gray}\G\vdash}\,p \overlap q}}
\begin{array}{ll@{\quad\qquad}ll}
\text{Reachability Relation} & {\color{gray}\G\vdash}\, x \reaches y \Leftrightarrow  x : T^{q,y} \in \Gamma &
\text{Variable Saturation} & {\color{gray}\G\vdash}\, \qsat{x} := \left\{\, y \mid x \reaches^* y\, \right\} \\[1.1ex]
\text{Qualifier Saturation} & {\color{gray}\G\vdash}\, \qsat{q} :=  \bigcup_{x\in q} \qsat{x} &
\text{Qualifier Overlap} & {\color{gray}\G\vdash}\,p \overlap q  := \qsat{p} \qglb \qsat{q} \\[1.1ex]
\text{Qualifier Separation} & {\color{gray}\G\ts}\,p \nonoverlap q := p \overlap q \subq\qbot
\end{array}$$
\judgement{Well-Formed Context, Types, Qualifiers}{\BOX{\G\textsf{~ok}}\ \BOX{\G\ts T,\cdots,q,\cdots}}
\begin{array}{l@{\qquad}l@{\ }l}
\text{Closed Context} & \qbot\textsf{~ok} & (\G, x: \ty[q]{T})\textsf{~ok} :=\FV(T),q\subq\dom(\G)\land\G\textsf{~ok} \\[1.1ex]
\text{Closed Types, Qualifiers} & \G\ts T,\cdots,q,\cdots &:= \FV(T),\cdots,q,\cdots\subq\dom(\G) \\
\end{array}$$
\end{mdframed}
\caption{Qualifier operations and closedness conditions in $\maybelang$. Sometimes the context $\G$ is implicit (in {\color{gray}gray}).
Taken and adapted from \cite{DBLP:journals/pacmpl/WeiBJBR24}.} \label{fig:qualops}
\vspace{-3ex}
\end{figure}
We further define substitution, reachability, saturation, and overlap of
qualifiers in \Cref{fig:qualops}. They shed light on the semantics of
reachability qualifiers and are key instruments to enforce aliasing and
separation in function applications as demonstrated in \Cref{sec:nutshell}.
Substitution intuitively supports dependent application, while saturation
supports the notion of separation. It presents an upper bound on the locations
a variable can
reach; thus, the intersection of two saturations are effectively
the upper bound on the overlap of the two variables.
We also present notations for well-formed contexts, types, and qualifiers in
\Cref{fig:qualops}.

\subsection{Typing} \label{sec:typing}

\begin{figure}[t]
\begin{mdframed}
\small
\judgement{Term Typing}{\BOX{\strut\G[\flt] \ts t : \ty{Q}}}\\%
\begin{minipage}[t]{.42\linewidth}\vspace{0pt}
\infrule[t-cst]{
c \in B
\G[\flt] \ts c : \ty[\qbot]{B}
\vgap
\infrule[t-var]{
x : \ty[q]{T} \in \G\quad\quad x \in \flt
\G[\flt] \ts x : \ty[x]{T}
\vgap
\infrule[t-ref]{
\G[\flt]\ts t : \ty[q]{B}%
\G[\flt]\ts \tref~t : \ty[\starred{q}]{(\TRef~\ty{B})}
\vgap
\infrule[t-deref]{
\G[\flt]\ts t : \ty[q]{(\TRef~\ty{B})}%
\G[\flt]\ts !t : \ty[\qbot]{B}
\vgap
\infrule[t-assgn]{
\G[\flt]\ts t_1 : \ty[q]{(\TRef~\ty{B})} \quad
\G[\flt]\ts t_2 : \ty[p]{B} %
\G[\flt]\ts t_1 \coloneqq t_2 : \ty[\qbot]{B}
\vgap
\infrule[t-sub]{
\G[\flt]\ts t : \ty{Q} \quad  \G[\flt]\ts\ty{Q} <:^\delta \ty[q]{T}\quad q\subq\starred{\flt}
\G[\flt]\ts t : \ty[q]{T}
\end{minipage}
\begin{minipage}[t]{.02\linewidth}
\hspace{1pt}%
\end{minipage}%
\begin{minipage}[t]{.54\linewidth}\vspace{0pt}
\infrule[t-abs]{
\cx[q,x]{(\G\ ,\ x: \ty[{p[q/f]}]{T})} \ts t : \ty[{r[q/f]}]{U}\\
\G\ts T,U,p_{\setminus f},q \quad \qfresh\notin q \\
\ty{F} = \ty[q]{\left(f(x: \ty[p]{T}) \to \ty[r]{U}\right)} \quad
p,q\subq \starred{f,\flt} \\
\G[\flt] \ts \lambda f(x).t : \ty{F}
\vgap
\infrule[t-app]{
\G[\flt]\ts t_1 : \ty[q]{\left(f(x: \ty[p]{T}) \to \ty[r]{U}\right)} \quad
\G[\flt]\ts t_2 : \ty[p']{T}\\
\QFresh\notin p\qquad r\subq\starred{\varphi,x,f}\\
p_1 = \text{if~} \isVar(t_1) \text{~then~} p[t_1/f] \text{~else~} p \\
\G[\flt]\ts p' <: p_1
\G[\flt]\ts t_1~t_2 : \ty[{r[p'/x, q/f]}]{U}
\vgap
\infrule[t-app$\QFresh$]{
\G[\flt]\ts t_1 : \ty[q]{\left(f(x: \ty[p]{T}) \to \ty[r]{U}\right)}\quad
\G[\flt]\ts t_2 : \ty[p']{T}\\
\QFresh \in p \qquad r\subq\starred{\varphi,x,f} \\
f\notin p \implies %
\G[\flt]\ts p' <: p''\ \land\ {p''}_{\setminus {p}}\nonoverlap q
\G[\flt]\ts t_1~t_2 : \ty[{r[p'/x, q/f]}]{U}
\vgap
\infrule[t-as]{
\G[\flt]\ts t : \ty[q]{T} \quad q\subq\starred{\flt}
\G[\flt]\ts (t: \ty[q]{T}) : \ty[q]{T}
\end{minipage}%
\end{mdframed}
\caption{Typing rules of $\maybelang$.} \label{fig:typing}
\vspace{-3ex}
\end{figure}
In \Cref{fig:typing}, we present the typing rules of $\maybelang$. Simple cases
include constants and variables. For constants \textsc{(t-cst)}, the empty qualifier is assigned
as primitive values track no non-trivial resources. The variable~$x$ in \textsc{(t-var)}, on the
other hand, is assigned the qualifier $x$. Such instantiation is ``lazy'' and leaves
room for subtyping to reveal the full reachability of $x$. Note that $x$ is
additionally required to reside in the observation $\flt$ to enforce separation.

Typing rules for reference operations are standard modulo the qualifiers. For
\textsc{(t-ref)}, we mark the result with~$\QFresh$ as it is a fresh
value. Results of dereference \textsc{(t-deref)} and assignment \textsc{(t-assgn)}, on the other hand, are
untracked (marked by $\qbot$), as we allow references only over base types.

Subsumption \textsc{(t-sub)} and ascription \textsc{(t-as)} are key rules for deriving bidirectional typing
algorithms. The declarative versions used here are standard, except that we require
the result qualifiers to remain inside the observation $\flt$.
Also, the subtyping relation comes with the growth marker $\delta$, which serves
subtyping derivations in \Cref{sec:subtyping} and plays no role here.

The abstraction rule \textsc{(t-abs)} features shallow dependencies of dependent variables.
While the argument qualifier $p$ can reach $f$ and the result qualifier $r$
can reach both $f$ and $x$, neither of their corresponding types $T, U$ can
reach any dependent variable, thus \textit{shallow}. This restriction
is only to make the type system concise and is not essential; we
further discuss how to remove it in \Cref{sec:deepdep}. On the other hand,
to type check the body, we restrict the observation to the
function qualifier~$q$ plus the argument~$x$. Thus, the argument is the only path
through which a function can access a value beyond its observation. As the
function itself is not in the context when typing the body, we eagerly substitute
the self-reference~$f$ with the qualifier~$q$. The argument and the
function qualifiers $p,q$ are further required to be within the observation $\flt$.

As demonstrated in \Cref{sec:nutshell}, there are two cases of
function application, differentiated by
whether fresh values are allowed as arguments. In the non-fresh
case \textsc{(t-app)}, we require the actual argument qualifier to be a
sub-qualifier of the formal one. If possible, we replace the self-reference $f$
in the formal argument with a proper closure variable rather than unfold it,
enforcing Lesson~\ref{lsn:negative}.
In the fresh case \textsc{(t-app$\qfresh$)},
we require that some upper bound ($p''$) of the actual argument qualifier ($p'$)
less the formal qualifier ($p$) does not overlap with the function
($q$). Said alternatively, everything in the actual argument is
either bounded by the formal qualifier or separated from the function
observation. Observing Lesson~\ref{lsn:arbitrary}, we check this condition
only if the self-reference is not in the argument qualifier, \ie $f\notin p$.
In both cases, we are doing dependent application, substituting
dependent variables $f,x$ with the actual qualifiers. As we require
shallow dependency for function types, the substitutions here are shallow as

In comparison with prior work \cite{DBLP:journals/pacmpl/WeiBJBR24}, we make
some simplifications in $\maybelang$:
(1) we support no nested references,
(2) we restrict the function types to shallow dependency, and
(3) we provide no support for type abstraction.
These features are orthogonal to our design,
as the key difficulties with self-references already appear in our simpler system.
Additionally, these simplifications do provide us with more
accessible typing rules, \eg \textsc{(t-app$\qfresh$)}. With the refined
subtyping relation, $\maybelang$ enjoys sound and decidable type checking (\Cref{sec:algo})
and is more expressive than the prior work (\Cref{sec:encode}, where we
also discuss how to add more features).

\subsection{Subsumption of Types, Qualifiers, and Qualified Types} \label{sec:subtyping}

\begin{figure}[t]
\small
\begin{mdframed}
\judgement{Subtyping}{\BOX{\strut \G[\flt]\ts\ty{Q} <:^{\delta}_{\color{gray}m} \ty{Q}}
\ \BOX{\strut\G[\flt] \ts q <:_{\color{gray}m} q}
\ \BOX{\strut \G[\flt]\ts\ty{T} <:^\delta \ty{T}}}\\
\begin{minipage}[t]{.5\linewidth}%
\smallskip
\infrule[sq-sub]{
\G[\flt]\ts T <:^\delta U \qquad \G[\flt]\ts p,\delta <: q
\G[\flt]\ts\ty[p]{T} <:^\delta \ty[q]{U}
\vgap
\infrule[sq-trans]{
\G[\flt]\ts\ty{P} <:^{\delta_1} \ty{Q} \qquad
\G[\flt]\ts\ty{Q} <:^{\delta_2} \ty{R}
\G[\flt]\ts\ty{P} <:^{\delta_1,\delta_2} \ty{R}
\vgap
\infrule[sq-mask]{
\G[\flt]\ts \ty[{p[\QFresh/m]}]{T} <:^\delta \ty[{q[\QFresh/m]}]{U} \qquad
p \subq_{\starred{m}} q
\G[\flt]\ts\ty[p]{T} <:^\delta_m \ty[q]{U}
\vgap
\infrule[s-base]{
\G[\flt]\ts B <:^\qbot B
\end{minipage}
\begin{minipage}[t]{.5\linewidth}%
\infrule[q-sub]{
p\subq q\subq \starred{\dom(\G)}
\G[\flt]\ts p <: q
\vgap
\infrule[q-var]{
x : \ty[q]{T}\in\G \quad \QFresh\notin q \quad
q\subq \flt
\G[\flt]\ts p <: p[q/x]
\vgap
\infrule[q-trans]{
\G[\flt]\ts p <: q \quad
\G[\flt]\ts q <: r
\G[\flt]\ts p <: r
\vgap
\infrule[q-mask]{
\G[\flt]\ts p_{\setminus m} <: q_{\setminus m} \qquad p \subq_m q
\G[\flt]\ts p <:_m q
\vgap
\infrule[s-ref]{
\G[\flt]\ts S <:^\varnothing T \qquad \G[\flt]\ts T <:^\varnothing S %
\G[\flt]\ts\ty{\TRef~S} <:^\qbot \ty{\TRef~T}
\end{minipage}\\
\infrule[s-fun]{
\G[\flt]\ts P_2 <:^\qbot_f P_1 \qquad
\G[\flt]\ts R_1 <:^{\delta_2}_{f,x} R_2
\G[\flt]\ts\ty{f(x: P_1) \to R_1} <:^\qbot \ty{f(x: P_2) \to R_2}
\infrule[s-depgr]{
\G[\flt]\ts\ty[{p_2}]{T_2} <:^{\delta_1}_f \ty[{p_1}]{T_1} \qquad
\G[\flt]\ts\ty[{r_1}]{U_1} <:^{\delta_2}_{f,x} \ty[{r_2}]{U_2} \\
x\in r_1 \implies \G[\flt]\ts {p_1}_{\setminus\starred{f}} <: {r_2}_{\setminus\starred{f,x}}
\G[\flt]\ts\ty{f(x: \ty[p_1]{T_1}) \to \ty[r_1]{U_1}} <:^\qbot \ty{f(x: \ty[p_2]{T_2}) \to \ty[r_2]{U_2}}
\infrule[s-negf]{
\G\ts T,R_{\setminus f,x},p_1,{p_2}_{\setminus f}
\G[\flt]\ts\ty{f(x:\ty[\starred{f,p_1}]{T})\to R} <:^\qbot \ty{f(x:\ty[p_2]{T})\to R}
\infrule[s-posx]{
\G\ts T,U \qquad
x\notin r_2\qquad \QFresh\notin p\qquad
\G[\flt]\ts p,r_1 <:_{f,x} r_2 %
\G[\flt]\ts\ty{f(x:\ty[p]{T})\to\ty[x,r_1]{U}} <:^\qbot \ty{f(x:\ty[p]{T})\to\ty[r_2]{U}}
\infrule[s-grow]{
f\in p\implies \QFresh\in p \qquad
\G\ts T,U,p_{\setminus f} \\
\delta\cap\{\starred{f,x}\}\subq\qbot \qquad
\G[\flt]\ts r_1 <:_{f,x} f,r_2,\delta
\G[\flt]\ts\ty{f(x:\ty[p]{T})\to\ty[r_1]{U}} <:^\delta \ty{f(x:\ty[p]{T})\to\ty[f,r_2]{U}}
\end{mdframed}
\caption{Subtyping rules of $\maybelang$.} \label{fig:subtype}
\vspace{-4ex}
\end{figure}
Taking the lessons from \Cref{sec:selfref}, we present
the subtyping rules of $\maybelang$ in \Cref{fig:subtype}. At a
high-level, the rules include those for qualified types
\textsc{(sq-$*$)}, qualifiers \textsc{(q-$*$)}, and types \textsc{(s-$*$)}.
Rules for types and qualified types include a notion of growth
$\delta$. Motivated by Lesson~\ref{lsn:growth},
it is a slice of qualifiers representing the minimum requirement
to the right hand side posted by type relations,
propagated from types to qualified types via \textsc{(sq-sub)}.\footnote{
In the mechanization, type relations
are always combined with \textsc{(sq-sub)}. Here we separate them
for clarity.} Qualified types also admit transitivity \textsc{(sq-trans)},
where the goal is considered growing if either step grows (\ie has a non-empty

Qualifier behavior is similar to that of sets, but as variable qualifiers can
be lazily instantiated by~\textsc{(t-var)}, additional rules are needed
to reason about their full reachability.
In this regard, \textsc{(q-sub)} reflects the subset relation for qualifiers,
and \textsc{(q-var)} allows us to unfold a variable $x$ if it is non-fresh.
Qualifiers also admit transitivity \textsc{(q-trans)} for chaining the former
two rules.

Rules for qualified types and qualifiers also optionally take a dependent
variable mask $m$.\footnote{The rules with masks do not appear in the
mechanization as they are always inlined.}
The rules \textsc{(sq-mask)} and \textsc{(q-mask)} allow us
to state subtyping relations over qualifiers with dependent variables which are
not in the typing context. They separate the dependent variables from the
qualifiers and check their subsumption respectively.
An alternative formal
development can definitely extend the typing context to include the dependent
variables without using the masks.

The non-qualified subtyping rules for base types \textsc{(s-base)} and references \textsc{(s-ref)} are mostly standard. They are
marked as non-growing rules by synthesizing empty growth $\qbot$, since they
carry no self-reference. \textsc{(s-ref)} further requires the data type to be non-growing and invariant.

The base case for function types \textsc{(s-fun)} is classic, where the
argument type is contravariant and the return type is covariant, with the
dependent variables marked in the masks. We do
restrict that the argument subtyping synthesizes no growth in observing
Lesson~\ref{lsn:depgr}. This constraint can be lifted as in
\textsc{(s-depgr)}, where we additionally require that the argument growth
Due to encoding issues in the mechanization, we use
$p_{\setminus\starred{f}}$ as an upper bound to $\delta_1$ here.}
is compensated in the right hand side result $r_2$
so that we lose no soundness in dependent applications.

Three additional function subtyping rules describe the behavior of
dependent variables in a position-specific way.
Backed by Lesson~\ref{lsn:arbitrary}, \textsc{(s-negf)} says that we can narrow the argument
qualifier arbitrarily if the left hand side permits anything. \textsc{(s-posx)} describes how to unfold the
dependent variable $x$ in the result qualifier, which is similar to \textsc{(q-var)} but under a
different context concerning the other dependent variable $f$. Reifying Lesson~\ref{lsn:growth},
\textsc{(s-grow)} is the only rule synthesizing a non-empty growth. It
describes that we can hide the result qualifier $r_1$ into the function
self-reference if the function's observation (here the growth $\delta$)
covers them, unless the self-references is also used in the negative position in
a non-growable way (\ie $f\in p\land\QFresh\notin p$). The transitivity rule
\textsc{(sq-trans)} is required to chain the function subtyping rules
for expressive behavior.

Comparing with the prior work~\cite{DBLP:journals/pacmpl/WeiBJBR24}, we remove
their rule for self-references as a standalone qualifier rule, since the
semantics of self-references makes no sense without the context of a function
type. We have different subtyping rules then for self-references in negative
\textsc{(s-negf)} and positive positions \textsc{(s-grow)}, and we use the
concept of growth $\delta$ to connect types and qualifiers. This finally
provides us with an expressive system involving self-references.

\subsection{Metatheory}

While we do not claim type soundness of $\maybelang$ as our major
contribution, we present the key result here without diving into the details. As
$\maybelang$ is a core calculus with extensions to subtyping compared with
the prior work~\cite{DBLP:journals/pacmpl/WeiBJBR24}, we believe that porting
the changes back into their system would not break their type soundness claims.
Thus, we refer curious readers to their work for a full establishment of
semantics and type soundness.
For the purpose of this work, we have mechanized proof in the flavor of logical
relations \cite{timanyLogicalApproachType,baoModelingReachabilityTypes2023}. %

\begin{theorem}[Fundamental]
A well-typed term $e$ with the qualified type $\ty[q]{T}$ under the context
$\G$ can be evaluated to a value $v$ of the type $\ty{T}$ on a store $\sigma$
in finite steps, where
$v$ can only reach the locations permitted by the qualifier $q$.
\end{theorem}

Our fundamental theorem implies the termination of well-typed terms in addition
to type soundness, and it further relates to
the progress, preservation, and preservation of separation
claims from \citet{DBLP:journals/pacmpl/WeiBJBR24},
provided the denotation of qualifiers into store locations.
Especially, if the qualifiers of two well-typed terms do not overlap, their
values surely observe separate locations.
While semantic and syntactic
type soundness proofs render their claims in distinct ways, we believe
$\maybelang$ can also be proven sound syntactically.
\section{Bidirectional Typing Algorithm} \label{sec:algo}

In accordance to the formal theory of $\maybelang$ presented in
\Cref{sec:lang}, in this section we discuss how to type check $\maybelang$ in a
sound and decidable way, concerning the challenges discussed in \Cref{sec:challenge}.
Here, we present the algorithm bottom up with metatheory
for individual parts as follows. The algorithm is mechanized as an executable
function in Coq along with its metatheory.%
\footnote{\artifact}

\newcommand*{\algout}[1]{{\color{purple}{#1}}}

\subsection{Qualifier Algorithms}

\begin{figure}[t]
\begin{mdframed}
\small
\judgement{Qualifier Upcast and Checking}{\BOX{\strut\G[\algout{\flt}] \ts q \ll^q \algout{q}}
\BOX{\strut\G[\algout{\flt}] \ts q < q}}\\%
\begin{minipage}[t]{.5\textwidth}
\infrule[qa-head]{
x\in p \quad x\notin r \quad \QFresh\notin q \\
\G[\algout{\flt}]\ts p[q/x] \ll^r \algout{p'}
\cx[\algout{\flt,q}]{(\G, x: \ty[q]{T})} \ts p \ll^r \algout{p'}
\vgap
\infrule[qa-skip]{
x\notin p \lor x\in r \lor \QFresh\in q \\
\G[\algout{\flt}]\ts p \ll^r \algout{p'}
\cx[\algout{\flt}]{(\G, x: \ty[q]{T})} \ts p \ll^r \algout{p'}
\end{minipage}
\begin{minipage}[t]{.5\textwidth}
\infrule[qa-nil]{}{
\cx[\algout{p}]{\qbot} \ts p \ll^r \algout{p}
\vgap
\infrule[qa-sub]{
\G[\algout{\flt}]\ts p \ll^r \algout{p'} \quad
p' \subq r
\G[\algout{\flt,r}] \ts p < r
\end{minipage}
\end{mdframed}
\caption{Algorithmic qualifier upcast and checking. Outputs in the rules are marked in \algout{red}.} \label{fig:algqual}
\vspace{-2ex}
\end{figure}
\Cref{fig:algqual} demonstrates the algorithms to upcast and check a qualifier
based on the sub-qualifier relation.
Both algorithms always synthesize the observation filter $\flt$.
Intuitively, the upcast algorithm
($\G[\algout{\flt}]\ts p\ll^r\algout{p'}$) recursively replaces variables in $p$
with their origins unless they are already within the boundary of $r$.
The checking algorithm ($\G[\algout{\flt}]\ts p<r$) then
utilizes the upcast algorithm to check whether the origin set
$p'$ is subsumed by $r$.
The upcast algorithm serves not only the checking algorithm,
but also the upper bound $p''$ in the fresh application case,
\ie \textsc{(t-app$\qfresh$)} in \Cref{fig:typing} and \textsc{(ta-app)} in
\Cref{fig:bidir}.
At a high-level, the rule
\textsc{(qa-head)} implements the declarative rule \textsc{(q-var)}, and
\textsc{(qa-sub)} implements \textsc{(q-sub)}. Transitivity is discharged by
enforcing the induction ordering along $\G$.
The algorithms enjoy the following metatheory,

\begin{lemma}[QualUpcast Soundness]
If $\G[\algout{\flt}]\ts p\ll^r \algout{p'}$
and the inputs are closed, \ie $\G\textsf{~ok}$ and $\G\ts p$,
then $\G[\flt]\ts p <: p'$ and
the outputs are closed, \ie $p' \subq \flt$ and $\G\ts\flt$.
\end{lemma}%
\begin{lemma}[QualCheck Soundness]
If $\G[\algout{\flt}]\ts p < r$
and the inputs are closed, \ie $\G\textsf{~ok}$ and $\G\ts p,r$,
then $\G[\flt]\ts p <: r$ and
the outputs are closed, \ie $r \subq \flt$ and $\G\ts\flt$.
\end{lemma}
\begin{lemma}[Qualifier Decidability]
Both algorithms finishes within finite steps.
\end{lemma}

\subsection{Subtype Checking}

\begin{figure}[t]
\begin{mdframed}
\small
\judgement{Subtype Checking}{\BOX{\strut\G[\algout{\flt}] \ts \ty{T} <^\algout{\delta} \ty{T}}}\\%
\begin{minipage}[t]{.4\linewidth}\vspace{0pt}
\infrule[sa-base]{}{
\G[\algout{\qbot}] \ts B <^\algout{\qbot} B
\end{minipage}
\begin{minipage}[t]{.03\linewidth}
\hspace{1pt}%
\end{minipage}%
\begin{minipage}[t]{.5\linewidth}\vspace{0pt}
\infrule[sa-ref]{
\G[\algout{\flt_1}]\ts a <^\algout{\qbot} b \quad
\G[\algout{\flt_2}]\ts b <^\algout{\qbot} a
\G[\algout{\flt_1,\flt_2}]\ts \TRef~a <^\algout{\qbot} \TRef~b
\end{minipage}
\infrule[sa-fun]{
\begin{array}{l@{\qquad}l@{\qquad}l}
p_2 \subq_{\starred{f}} p_1 &
\G[\algout{\flt_1}] \ts T_2 <^\algout{\delta_1} T_1 &
p_1' = {p_2}_{\setminus\starred{f}},\delta_1 \\
r_1 \subq_{\starred{f}} r_2 &
\G[\algout{\flt_2}] \ts U_1 <^\algout{\delta_2} U_2 &
r_2' = {r_1}_{\setminus\starred{f,x}},\delta_2 \\
\end{array} \\
\begin{array}{l@{\ }lc}
\delta_1' = \left\{\begin{array}{l}
p_1', \\
\qbot,
\end{array}\right. &
\begin{array}{l}
\text{if~}x\in r_1 \land \delta_1\neq\qbot; \\
\text{otherwise}
\end{array} &
{\color{gray}\textsc{(s-depgr)}} \\
p_2' = \left\{\begin{array}{l}
\qbot, \\
{p_2}_{\setminus f},   \\
\bot,
\end{array}\right. &
\begin{array}{l}
\text{if~}x\in r_1 \implies x\in r_2; \\
\text{else if~}\qfresh\notin p_2 \land (f\in p_2\implies f\in r_2); \\
\text{otherwise}
\end{array} &
\end{array} \\
r_2'' = r_2', \delta_1', {p_2'} \\
\begin{array}{l@{\ }lc}
\left\{\begin{array}{l}
\algout{\flt_1'} = \qbot, \\
\G[\algout{\flt_1'}]\ts p_1' < {p_1}_{\setminus\starred{f}},
\end{array}\right. &
\begin{array}{l}
\text{if~}\starred{f}\subq p_1; \\
\text{otherwise}
\end{array} &
{\color{gray}\textsc{(s-negf)}} \\
\left\{\begin{array}{l}
\algout{\delta} = \qbot, \\
\algout{\flt_2'} = \algout{\delta} = r_2'', \\
\bot,
\end{array}\right. &
\begin{array}{ll}
\text{if~}\G[\algout{\flt_2'}]\ts r_2'' < {r_2}_{\setminus\starred{f,x}}; \\
\text{else if~}f\in r_2 \land (f\in p_2\implies \qfresh\in p_2); \\
\text{otherwise}
\end{array} &
\end{array}
\G[\algout{\flt_1,\flt_1',\flt_2,\flt_2'}]\ts f(x: \ty[p_1]{T_1}) \to \ty[r_1]{U_1} <^\algout{\delta} f(x: \ty[p_2]{T_2}) \to \ty[r_2]{U_2}
\end{mdframed}
\caption{Algorithmic subtype checking. Outputs are marked in \algout{red}.} \label{fig:subcheck}
\vspace{-3ex}
\end{figure}
\Cref{fig:subcheck} presents the algorithm for checking subtype relations.
The algorithm takes two types as inputs and always synthesizes the filter $\flt$
and the growth $\delta$. While \textsc{(sa-base)} and \textsc{(sa-ref)} are
obvious from their declarative versions, \textsc{(sa-fun)} packs the multiple
function rules into one, discharging the transitivity. It first checks the
subtype of the argument types and the result types, contravariant and covariant
accordingly. It then synthesizes $\delta_1'$ if \textsc{(s-depgr)} is
applicable, and $p_2'$ if \textsc{(s-posx)} is applicable. Next, it constructs
$p_1'$ and $r_2''$ for qualifier checking. It checks $p_1'$ against $p_1$ unless
\textsc{(s-negf)} is applicable, and then $r_2''$ against $r_2$, try applying
\textsc{(s-grow)} on failure. The algorithm enjoys the following metatheory,

\begin{lemma}[SubCheck Soundness]
If~$\G[\algout{\flt}]\ts T_1 <^\algout{\delta} T_2$
and the inputs are closed, \ie $\G\textsf{~ok}$ and $\G\ts T_1, T_2, q$,
then $\G[\flt]\ts \ty[q]{T_1} <:^\delta \ty[q,\delta]{T_2}$
and the outputs are closed, \ie $\delta\subq\flt$ and $\G\ts\flt$.
\end{lemma}
\begin{lemma}[SubCheck Decidability]
The subtype checking algorithm finishes in finite steps.
\end{lemma}

\subsection{Avoidance}

\begin{figure}[t]
\begin{mdframed}
\small
\judgement{Avoidance}{\BOX{\strut\cx[\algout{\flt}]{} \ts \ty{T} \le_a^{\algout{\delta}} \algout{\ty{T}}}
\BOX{\strut\cx[\algout{\flt}]{} \ts \ty{T} \ge_a^{\algout{\delta}} \algout{\ty{T}}}
\BOX{\strut\cx[\algout{\flt}]{} \ts \ty{T} \ge_a^\bot \algout{\ty{T}}}}\\%
\begin{minipage}{.4\linewidth}
\infrule[av-base]{}{
\cx[\algout{\qbot}]{}\ts \ty{B} \le_a^{\algout{\qbot}} \algout{\ty{B}} \\
\cx[\algout{\qbot}]{}\ts \ty{B} \ge_a^{\algout{\qbot}} \algout{\ty{B}} \\
\cx[\algout{\qbot}]{}\ts \ty{B} \ge_a^\bot \algout{\ty{B}}
\end{minipage}
\begin{minipage}{.5\linewidth}
\infrule[av-ref]{
\cx[\algout{\flt}]{}\ts \ty{T} \le_a^{\algout{\delta}} \algout{\ty{T'}} \qquad
T \equiv T'
\cx[\algout{\qbot}]{}\ts \TRef~\ty{T} \le_a^{\algout{\qbot}} \algout{\TRef~\ty{T}} \\
\cx[\algout{\qbot}]{}\ts \TRef~\ty{T} \ge_a^{\algout{\qbot}} \algout{\TRef~\ty{T}} \\
\cx[\algout{\qbot}]{}\ts \TRef~\ty{T} \ge_a^\bot \algout{\TRef~\ty{T}}
\end{minipage}
\infrule[av-posf]{
\left\{\begin{array}{ll}
\cx[\algout{\flt_1}]{}\ts T \ge_a^{\algout{\delta_1}} \algout{T'}, & \text{if~}\starred{f}\subq p; \\
\cx[\algout{\flt_1}]{}\ts T \ge_a^\bot \algout{T'} \land \algout{\delta_1} = \qbot, & \text{otherwise}
\end{array}\right. \qquad {\color{gray}\textsc{(s-negf)}} \\
\cx[\algout{\flt_2}]{}\ts U \le_a^{\algout{\delta_2}} \algout{U'} \\
\begin{array}{l@{}llc}
\algout{\delta} & = \left\{\begin{array}{l}
\delta_2,r_{\cap a},p_{\setminus\starred{f}},\delta_1, \\
\delta_2,r_{\cap a},
\end{array}\right. &
\begin{array}{l}
\text{if~}\delta_1\neq\qbot \land x\in r; \\
\text{otherwise}
\end{array} &
{\color{gray}\textsc{(s-depgr)}} \\
\algout{p'} & = \left\{\begin{array}{l}
p_{\setminus{f,a}}, \\
p_{\setminus a},
\end{array}\right. &
\begin{array}{l}
\text{if~}\delta\neq\qbot \land \qfresh\notin p; \\
\text{otherwise}
\end{array} &
{\color{gray}\textsc{(s-grow)}} \\
\algout{r'} & = \left\{\begin{array}{l}
r_{\setminus a},f, \\
\end{array}\right. &
\begin{array}{l}
\text{if~}\delta\neq\qbot; \\
\text{otherwise}
\end{array} &
\end{array}
\cx[\algout{\flt_1,\flt_2,\delta}]{}\ts f(x: \ty[p]{T})\to\ty[r]{U} \le_a^{\algout{\delta}} f(x: \algout{\ty[p']{T'}}) \to \algout{\ty[r']{U'}}
\infrule[av-negf-ng]{
\cx[\algout{\flt_1}]{}\ts T \le_a^{\algout{\delta_1}} \algout{T'} \qquad
\cx[\algout{\flt_2}]{}\ts U \ge_a^\bot \algout{U'} \\
\begin{array}{l@{}llc}
\algout{p'} & = \left\{\begin{array}{l}
\starred{f},p_{\setminus a}, \\
\end{array}\right. &
\begin{array}{l}
\text{if~}\delta_1\neq\qbot \lor a\in p; \\
\text{otherwise}
\end{array} &
{\color{gray}\textsc{(s-negf)}} \\
\algout{r'} & = \left\{\begin{array}{l}
r_{\setminus {x,a}}, \\
r_{\setminus a},
\end{array}\right. &
\begin{array}{l}
\text{if~}\delta_1\neq\qbot \lor a\in p; \\
\text{otherwise}
\end{array} &
{\color{gray}\lnot\textsc{(s-depgr)}} \\
\algout{\delta} & = \left\{\begin{array}{l}
\qbot, \\
\bot,
\end{array}\right. &
\begin{array}{l}
\text{if~}f \notin r \lor f \in p\land \qfresh\notin p; \\
\text{otherwise}
\end{array} &
\end{array}
\cx[\algout{\flt_1,\flt_2}]{}\ts f(x: \ty[p]{T})\to\ty[r]{U} \ge_a^\bot f(x: \algout{\ty[p']{T'}}) \to \algout{\ty[r']{U'}} \\
\cx[\algout{\flt_1,\flt_2}]{}\ts f(x: \ty[p]{T})\to\ty[r]{U} \ge_a^{\algout{\delta}} f(x: \algout{\ty[p']{T'}}) \to \algout{\ty[r']{U'}}
\infrule[av-negf-gr]{
f\in p \implies \qfresh\in p \qquad {\color{gray}\textsc{(s-grow)}} \\
\cx[\algout{\flt_1}]{}\ts T \le_a^{\algout{\delta_1}} \algout{T'} \qquad
\cx[\algout{\flt_2}]{}\ts U \ge_a^{\algout{\delta_2}} \algout{U'} \\
\begin{array}{l@{}llc}
\delta_1' & = \left\{\begin{array}{l}
p_{\setminus\starred{f}},\delta_1, \\
\qbot,
\end{array}\right. &
\begin{array}{l}
\text{if~}\delta_1\neq\qbot \lor a\in p; \\
\text{otherwise}
\end{array} &
{\color{gray}\textsc{(s-depgr)}} \\
\algout{p'} & = \left\{\begin{array}{l}
\starred{f},p_{\setminus a}, \\
\end{array}\right. &
\begin{array}{l}
\text{if~}\delta_1'\neq\qbot; \\
\text{otherwise}
\end{array} &
{\color{gray}\textsc{(s-negf)}} \\
\algout{r'} & = \left\{\begin{array}{l}
r_{\setminus a},x, \\
r_{\setminus a},
\end{array}\right. &
\begin{array}{l}
\text{if~}\delta_1'\neq\qbot \land \qfresh\notin p; \\
\text{otherwise}
\end{array} &
{\color{gray}\textsc{(s-depgr) (s-posx)}} \\
\algout{\delta} & = \left\{\begin{array}{l}
\delta_1',\delta_2, \\
\delta_2,
\end{array}\right. &
\begin{array}{l}
\text{if~}x\in r'; \\
\text{otherwise}
\end{array} &
{\color{gray}\textsc{(s-depgr) (s-grow)}}
\end{array} \\
\cx[\algout{\flt_1,\flt_2,\delta}]{}\ts f(x: \ty[p]{T})\to\ty[f,r]{U} \ge_a^{\algout{\delta}} f(x: \algout{\ty[p']{T'}}) \to \algout{\ty[r']{U'}}
\end{mdframed}
\caption{The avoidance algorithm. Outputs are marked in \algout{red}.}
\label{fig:avoidance}
\vspace{-3ex}
\end{figure}
Presented in \Cref{fig:avoidance}, the avoidance algorithm
$\cx[\algout{\flt}]{}\ts T_1\le^{\algout{\delta}}_a \algout{T_2}$ removes all
occurrences of the variable~$a$ within the type $T_1$,
making up a larger type $T_2$ at the growth $\delta$ and the filter $\flt$.
It is needed to infer types for let-bindings and function bodies.
The cases for base types \textsc{(av-base)} and references \textsc{(av-ref)}
are trivial as they are always invariant and carry no free variable.
For functions, intuitively, we need to recursively replace $a$ with the
self-reference in covariant positions, and remove $a$ in contravariant positions. The growth $\delta$ then needs to carry $a$ to allow the avoidance.
To reify that, the case of function is
split into three cases with two auxiliary forms.

The positive rule \textsc{(av-posf)} recurs into the result type and calls
one of the negative rules on the argument type, permitting growth
if \textsc{(s-negf)} is applicable.
calculates the output growth~$\delta$ based on whether dependent application
\textsc{(s-depgr)} applies. It then removes $a$ from both the argument and
result qualifiers, and
inserts or removes the self-reference~$f$
to propagate $\delta$ by \textsc{(s-grow)}.

The non-growing negative rule \textsc{(av-negf-ng)}
recurs into the result type and calls the positive rule on the argument type.
The argument growth $\delta_1$ is always accommodated via \textsc{(s-negf)},
and the dependent argument $x$ %
may have to be removed so as not to propagate $\delta_1$ via \textsc{(s-depgr)}.
The growing negative rule \textsc{(av-negf-gr)}
differs from the former case in that
it always tries to propagate~$\delta_1$ by adding $x$ in the
result, as long as it is removable by \textsc{(s-posx)}.

Obviously, there is no principal avoidance algorithm for $\maybelang$.
Without diving into the auxiliary forms, we present the metatheory of
the main form of the avoidance algorithm as follows,

\begin{lemma}[Avoidance Soundness]
If~$\cx[\algout{\flt}]{}\ts T \le^{\algout{\delta}}_a \algout{T'}$,
the inputs are closed, \ie $(\G, a: Q)\ts T, q$,
then $\cx[\flt]{(\G,a: Q)}\ts \ty[q]{T} <:^\delta \ty[q,\delta]{T'}$
and the outputs are closed, \ie $\G\ts T'$, $(\G, a: Q)\ts \flt$ and $\delta\subq\flt$.
\end{lemma}
\begin{lemma}[Avoidance Decidability]
The avoidance algorithm finishes in finite steps.
\end{lemma}

\subsection{Bidirectional Typing}

\begin{figure}[t]
\begin{mdframed}
\small
\judgement{Bidirectional Typing}{\BOX{\strut\G[\algout{\flt}] \ts t \Leftarrow \ty{Q}}
\BOX{\strut\G[\algout{\flt}] \ts t \Leftarrow \ty[\Rightarrow \algout{q}]{T}}
\BOX{\strut\G[\algout{\flt}] \ts t \Rightarrow \algout{\ty{Q}}}}\\%
\begin{minipage}[t]{.47\linewidth}\vspace{0pt}
\infrule[ta-var]{
x : \ty[q]{T} \in \G
\G[\algout{x}] \ts x \Rightarrow \algout{\ty[x]{T}}
\vgap
\infrule[ta-cst]{
c \in B
\G[\algout{\qbot}] \ts c \Rightarrow \algout{\ty[\qbot]{B}}
\vgap
\infrule[ta-ref]{
\G[\algout{\flt}]\ts t \Rightarrow \algout{\ty[q]{B}}%
\G[\algout{\flt}]\ts \tref~t \Rightarrow \algout{\ty[\starred{q}]{(\TRef~\ty{B})}}
\vgap
\infrule[ta-deref]{
\G[\algout{\flt}]\ts t \Rightarrow \algout{\ty[q]{(\TRef~\ty{B})}}%
\G[\algout{\flt}]\ts !t \Rightarrow \algout{\ty[\qbot]{B}}
\vgap
\infrule[ta-assgn]{
\G[\algout{\flt_1}]\ts t_1 \Rightarrow \algout{\ty[q]{(\TRef~\ty{B})}} \quad
\G[\algout{\flt_2}]\ts t_2 \Rightarrow \algout{\ty[p]{B}} %
\G[\algout{\flt_1,\flt_2}]\ts t_1 \coloneqq t_2 \Rightarrow \algout{\ty[\qbot]{B}}
\vgap
\infrule[ta-subc]{
\G[\algout{\flt_1}]\ts t \Leftarrow \ty[\Rightarrow \algout{q'}]{T} \quad
\G[\algout{\flt_2}]\ts q' < q
\G[\algout{\flt}]\ts t \Leftarrow \ty[q]{T}
\vgap
\infrule[ta-subi]{
\G[\algout{\flt_1}]\ts t \Rightarrow \algout{\ty[q]{T'}} \quad
\G[\algout{\flt_2}]\ts T' <^\algout{\delta} T
\G[\algout{\flt_1,\flt_2}]\ts t \Leftarrow \ty[\Rightarrow \algout{q,\delta}]{T}
\vgap
\infrule[ta-as]{
\G\ts \ty[q]{T} \quad \G[\algout{\flt}]\ts t \Leftarrow \ty[q]{T}
\G[\algout{\flt}]\ts (t: \ty[q]{T}) \Rightarrow \algout{\ty[q]{T}}
\end{minipage}%
\begin{minipage}[t]{.03\linewidth}
\hspace{1pt}%
\end{minipage}%
\begin{minipage}[t]{.5\linewidth}\vspace{0pt}
\vgap
\infrule[ta-abs]{
r' = \text{if~} f\in p \text{~then~} r \text{~else~} r[q/f] \\
x' = \text{if~}\QFresh\notin p \land p\subq r' \text{~then~} x \text{~else~} \qbot \\
\cx[\algout{\flt}]{(\G\ ,\ x: \ty[{p[q/f]}]{T})} \ts t \Leftarrow \ty[{x',r[q/f]}]{U} \\
\flt\subq q,x
\G[\algout{p,q}] \ts \lambda f(x).t \Leftarrow \ty[q]{\left(f(x: \ty[p]{T}) \to \ty[r]{U}\right)}
\vgap
\infrule[ta-let]{
\G[\algout{\flt_2}]\ts t_2 \Rightarrow \algout{\ty[p]{T}} \quad
\cx[\algout{\flt_1}]{(\G, x: \ty[p]{T})}\ts t_1 \Rightarrow \algout{\ty[r]{U}} \\
\cx[\algout{\flt'}]{}\ts U \le^{\algout{\delta}}_{x} V \quad
\algout{\flt} = (\flt_2,\flt_1,\flt',p,r,\delta)_{\setminus\starred{x}}
\G[\algout{\flt}]\ts (\lambda f(x).t_1)~t_2 \Rightarrow \algout{V^{(r,\delta)[p/x]}}
\vgap
\infrule[ta-app]{
\G[\algout{\flt_1}]\ts t_1 \Rightarrow \algout{\ty[q]{\left(f(x: \ty[p]{T}) \to \ty[r]{U}\right)}} \\
\G[\algout{\flt_2}]\ts t_2 \Leftarrow \ty[\Rightarrow \algout{p'}]{T} \\
\left\{\begin{array}{l@{\ }l@{}}
\G[\algout{\flt'}]\ts p' < p, & \text{if~}\qfresh\notin p\land\lnot \isVar(t_1); \\[1ex]
\G[\algout{\flt'}]\ts p' < p_{[t_1/f]}, & \text{else if~}\qfresh\notin p\land \isVar(t_1); \\[1ex]
\begin{array}{@{}l}
\G[\algout{\flt'}]\ts p' \ll^p \algout{p''} \\[-.2ex]
\qquad\land\ {p''}_{\setminus p}\nonoverlap q,
\end{array} & \text{else if~}\qfresh\in p \land f\notin p; \\[2ex]
\algout{\flt'} = \qbot, & \text{otherwise}
\end{array}\right. \\
\algout{\flt} = \flt_1,\flt_2,\flt',r_{\setminus\starred{f,x}}
\G[\algout{\flt}]\ts t_1~t_2 \Rightarrow \algout{\ty[{r[p'/x, q/f]}]{U}}
\end{minipage}
\end{mdframed}
\caption{Bidirectional typing rules for $\maybelang$. Outputs are marked in \algout{red}.} \label{fig:bidir}
\vspace{-3ex}
\end{figure}
We finally present the top-level
typing algorithm in \Cref{fig:bidir}, %
bidirectionalized from \Cref{fig:typing} based on recipes
from \citet{DBLP:journals/csur/DunfieldK21}.
Our bidirectional typing algorithm actually comes with three
modes, checking~($\Leftarrow$), inference~($\Rightarrow$),
and one extra with simultaneous input and output~($\Leftarrow^\Rightarrow$)
\cite{DBLP:conf/pldi/PolikarpovaKS16},
checking the type and synthesizing the qualifier. This mode is used for
dependent application in \textsc{(ta-app)}.
On adding it, the algorithm enjoys two separate subsumption
rules \textsc{(ta-subc) (ta-subi)} to switch from checking to inference.
The ascription rule \textsc{(ta-as)}\footnote{
Due to encoding issues in mechanization, the closedness of the annotation is not checked, but supplied as a precondition.
} further enables switching from inference to
checking by explicit annotation.

Following the common approach, the algorithm
checks for abstractions \textsc{(ta-abs)} and
synthesizes for applications \textsc{(ta-app)}.
Abstractions then need to be accompanied
by annotations for types to be inferred,
with the exception made for let-bindings \textsc{(ta-let)}, where we
synthesize a type for the abstraction body and then use the avoidance algorithm
to remove the the binding variable.
The application rule \textsc{(ta-app)} combines the two declarative
rules. It infers a type from the function, and then
checks it against the argument, hopefully synthesizing a smaller
qualifier. The qualifier upcast algorithm ($\G[\algout{\flt}]\ts q\ll^q \algout{q}$) is used to provide
the upper bound in the fresh application case.

The soundness of the three modes should be stated in accordance as follows,

\begin{theorem}[Bidirectional Soundness]
If $\G[\algout{\flt}]\ts t\Leftarrow \ty[q]{T}$,
$\G[\algout{\flt}]\ts t\Leftarrow \ty[\Rightarrow\algout{q}]{T}$, or
$\G[\algout{\flt}]\ts t\Rightarrow \algout{\ty[q]{T}}$,
and the inputs are closed, \ie $\G\textsf{~ok}$
and $\G\ts T, q$ (only if provided as inputs),
then $\G[\flt]\ts t: \ty[q]{T}$ and the outputs are closed, \ie $\G\ts\flt$.
\end{theorem}
\begin{theorem}[Bidirectional Decidability]
The typing algorithm finishes in finite steps.
\end{theorem} %
\section{Case Study: Church-Encoded Pairs} \label{sec:encode}

The non-emptiness of the typing algorithm is best to be demonstrated with concrete
examples. In this section, we showcase how to write a simple program involving
Church-encoded pairs. Not only is the pair essential to day-to-day
programming, but it also presents a non-trivial higher-order program.
Furthermore, we discuss how to extend the core calculus $\maybelang$ to enrich
its behavior.

To get started, we demonstrate a snippet below making use of pairs.
As $\maybelang$ is a monomorphic calculus, we need to provide type parameters
to the constructor and eliminators,
and instantiate their definitions inside the snippets.
We further discuss polymorphism extensions in \Cref{sec:poly}.

\begin{lstlisting}
val p2 = {
val tr = ref true
val fl = ref false
val p1 = Pair[Ref[Bool]](tr, fl)  // p1: transparent pair with precise eliminations
val tr1 = fstT[Ref[Bool]$\trackvar{tr}$](p1)     // tr1: Ref[Bool]$\trackvar{tr}$
val fl1 = sndT[Ref[Bool]$\trackvar{fl}$](p1)     // fl1: Ref[Bool]$\trackvar{fl}$
p1                                // avoidance required
}                                   // p2: opaque pair with imprecise eliminations
val tr2 = fstO[Ref[Bool]](p2)       // tr2: Ref[Bool]$\trackvar{p2}$
val fl2 = sndO[Ref[Bool]](p2)       // fl2: Ref[Bool]$\trackvar{p2}$
\end{lstlisting}

With two named references, @tr,fl@, we can first construct a \emph{transparent}
pair @p1@, which supports precise elimination by @fstT,sndT@, resulting in
two separate references with qualifiers @tr@ and @fl@, respectively.
By ending the scope of @p1@, we then need to type @p2@ without mentioning
@tr,fl@, effectively producing an \emph{opaque} pair. We can no longer
differentiate the two components of the opaque @p2@, but to state that
both components are part of @p2@ by the opaque eliminators<EMAIL_ADDRESS>
\subsection{The Way of Transparency}

Here we give details to the forms of transparent
pairs. The constructor below unfolds
to a function @p@ taking an eliminator @f@ as argument. %
As the current algorithm requires, @p@ is accompanied with annotations
for later inference in applications.
As the result qualifier depends on the eliminator,
we can minimize the result by providing minimal eliminators.

\begin{lstlisting}
Pair[T](a, b) $\triangleq$
fn p(f: (f(x: T$\trackvar{a}$) => (g(y: T$\trackvar{b}$) => T$\trackvar{g}$)$\trackvar{f}$)$\trackvar{\qfresh p}$)$\trackset{a,b}$: T$\trackvar{f}$ => f(a)(b)
\end{lstlisting}

By the eliminator typing, they take in the two components as arguments by
precise qualifiers (@a,b@), and return a component reaching themselves (@g,f@).
As seen in Lesson~\ref{lsn:growth}, they can actually be returning one of their
arguments which is covered by the function observation.
Checked by \textsc{(ta-abs)} and \textsc{(ta-app)}, possible eliminators
include @fstT@ and<EMAIL_ADDRESS>They unfold to applying the actual eliminator
function to the pair<EMAIL_ADDRESS>
\begin{minipage}{.45\linewidth}
\begin{lstlisting}
fstT[T$\trackvar{a}$](p) $\triangleq$
p(fn f(x: T$\trackvar{a}$)$\trackvar{a}$ =>
fn g(y: T$\trackvar{\qfresh{g}}$)$\trackvar{f}$: T$\trackvar{g}$ => x)
\end{lstlisting}
\end{minipage}
\begin{minipage}{.5\linewidth}
\begin{lstlisting}
sndT[T$\trackvar{b}$](p) $\triangleq$
p(fn f(x: T$\trackvar{\qfresh{f}}$)$\trackvar{b}$ =>
fn g(y: T$\trackvar{b}$)$\trackvar{f}$: T$\trackvar{g}$ => y)
\end{lstlisting}
\end{minipage}

Both eliminator functions reach only one component in the qualifier, and take only one
argument by precise qualifier, the other arbitrarily. While such argument types
do not exactly match the requirement of the introduction form, the application
algorithm \textsc{(ta-app)} would invoke \textsc{(sa-fun)} to check the
Justified by \textsc{(s-negf)}, the algorithm would synthesize no growth.
Thus, by dependent application, we get precise results for transparent

\subsection{Avoidance to Opaque}

To produce the opaque pair type from the transparent @p1@, the algorithm
\textsc{(ta-let)} employs the avoidance algorithm to remove occurrences of
<EMAIL_ADDRESS>For their positive occurrences on the qualifiers of @x,y@,
\textsc{(av-negf-gr)} replaces them with self-references @f,g@, and propagates
the argument growth to the eliminator results by adding @x,y@ in the qualifiers.
The two steps together synthesizes a growth of @{tr,fl}@ towards @f@,
which, due to dependent application, must be compensated on the result qualifier.
Thus, \textsc{(av-posf)} adds the self-reference @p@ to the result.

\begin{lstlisting}
val p2 = {
p1  // (p(f: (f(x: T$\trackvar{tr}$) => (g(y: T$\trackvar{fl}$) => T$\trackvar{\phantom{\{}g\phantom{,y\}}}$)$\trackvar{\phantom{\{}f\phantom{,x\}}}$)$\trackvar{\qfresh{p}}$) => T$\trackvar{\phantom{\{}f\phantom{,p\}}}$)$\trackset{tr,fl}$
}     // (p(f: (f(x: T$\trackvar{\qfresh{f}}$) => (g(y: T$\trackvar{\qfresh{g}}$) => T$\trackset{g,y}$)$\trackset{f,x}$)$\trackvar{\qfresh{p}}$) => T$\trackset{f,p}$)$\trackset{tr,fl}$
\end{lstlisting}

Corresponding to the type change in the pair, we need also new eliminator
typings. The following opaque eliminators take in both arguments arbitrarily,
and by the types can return either argument or something observable from the
functions. The overall pair elimination further returns a component reaching
either the eliminator or the pair itself. As both eliminators carry empty
observations, such opaque eliminations always produce a result reaching @p2@

\begin{minipage}{.45\linewidth}
\begin{lstlisting}
fstO[T](p) $\triangleq$
p(fn f(x: T$\trackvar{\qfresh{f}}$)$\track$ =>
fn g(y: T$\trackvar{\qfresh{g}}$)$\trackset{f,x}$: T$\trackset{g,y}$ => x)
\end{lstlisting}
\end{minipage}
\begin{minipage}{.5\linewidth}
\begin{lstlisting}
sndO[T](p) $\triangleq$
p(fn f(x: T$\trackvar{\qfresh{f}}$)$\track$ =>
fn g(y: T$\trackvar{\qfresh{g}}$)$\trackset{f,x}$: T$\trackset{g,y}$ => y)
\end{lstlisting}
\end{minipage}

\subsection{Reaching Beyond $\maybelang$}

While the above examples are all expressible by $\maybelang$ and checkable by
the algorithm from \Cref{sec:algo}, $\maybelang$ is just a simplistic calculus
on its own. Here we discuss some useful extensions to the language and the

\subsubsection{Checking Functions as Arguments}

One may suggest that the type instantiations for the eliminators can be removed
and instead supplied by inferred types from the pairs, as commonly seen in
local typing approaches \cite{DBLP:conf/popl/OderskyZZ01,DBLP:journals/csur/DunfieldK21}.
However, our \textsc{(ta-app)} requires the argument qualifier to be
synthesized, while \textsc{(ta-abs)} need the function qualifier as input to
drive its type checking.
This conflict can be alleviated by additional rules to
synthesize qualifiers for functions. Alternatively, proper type-and-qualifier
abstraction can also help to remove this instantiation, provided a
solution for type parameter instantiation.

\subsubsection{Polymorphism} \label{sec:poly}

Orthogonal to this work, \citet{DBLP:journals/pacmpl/WeiBJBR24} has investigated
adding bounded quantification to reachability types. Even without quantifiers,
their monomorphic calculus has enjoyed a lightweight form of qualifier
polymorphism, which we choose to base $\maybelang$ on and suffices to support
precise component retrieval in pairs.
Implementation-wise, partial type reconstruction for System $F_{<:}$
has been widely studied. \citet{DBLP:journals/toplas/PierceT00,DBLP:conf/popl/OderskyZZ01} discussed solving the instantiation
problem by local constraint solving, while \citet{cardelli1993implementation}
investigated greedy inference, which works well in practice and was further proven
complete for System F \cite{DBLP:conf/icfp/DunfieldK13}.
Our work also builds a prototype for System $F_{<:}$
with reachability types beyond the mechanization, which enjoys some basic
forms of greedy instantiation.

\subsubsection{Deep Dependencies} \label{sec:deepdep}

The above examples can all be typed with the shallow dependency restriction
(cf. \Cref{sec:typing}). Still, it would be desirable if we can restore deep
dependencies. Most importantly, the
avoidance algorithm would then only be required for fresh applications
as showcased in \Cref{sec:selfref}, which can improve the precision of
reachability tracking and make type inference less demanding.
To do so, we first need to adapt the subtyping rules to make them
polarity-aware, as self-references may now occur deeply inside a type.
Secondly, we can further tweak the avoidance algorithm as more intuitive
solutions are now permitted.

\section{Effect Extensions} \label{sec:exten}
Reachability types can be layered with an effect system, \eg, to
enable non-trivial compiler optimizations via dependency
If the effect system is flow-sensitive, even finer-grained behaviors
can be tracked,
\eg, move semantics and ownership transfer~\cite{DBLP:journals/pacmpl/BaoWBJHR21}.
In this section, we discuss inferring/checking effects by extending the bidirectional
typing algorithm presented in \secref{sec:algo}.
While not part of the corresponding Coq development, these extensions
have all been implemented in a prototype
and validated experimentally.

\bfparagraph{Flow-Insensitive Store Effects} Reachability types can be extended with
a flow-insensitive effect system,
tracking read/write effects (``use`` effects) on reachable references~\cite{DBLP:journals/pacmpl/BaoWBJHR21,oopsla23,oopsla23supplement}.
Consider the following example, where variables @x@ and @y@ are aliased.
\begin{lstlisting}
val x = ref 42; val y = x; val z = ref 1
y := !y + 1       // Int @wr(y) in context [z: Ref[Int]$\trackfresh$, y: Ref[Int]$\trackvar{x}$, x: Ref[Int]$\trackfresh$]
\end{lstlisting}
Incrementing the content of @y@ by 1 induces a write effect (@≠wr@) on variable @y@,
and transitively on @x@ too, but not on<EMAIL_ADDRESS>The preservation of separation corollary~\cite{DBLP:journals/pacmpl/WeiBJBR24} guarantees
that the transitive separation of reachable variables (separation for short) from @y@ and @z@
implies the separation of their eachable store locations.
Thus, such an effect system can be used to show that values (\eg, the referent of @z@) are preserved over a potential effectful computation~\cite{oopsla23supplement}.

\bfparagraph{Flow-Sensitive Move Effects}
The effect system can further be extended to be flow-sensitive, tracking destructive ``move'' effects~\cite{DBLP:journals/pacmpl/BaoWBJHR21},\footnote{The ``move'' effects are called ``kill'' effects in \citet{DBLP:journals/pacmpl/BaoWBJHR21}'s work.}
to enable expressing behaviors such as ownership transfer and properties like uniqueness.
In the following example, we extend $\maybelang$ with a primitive $\tmove$-expression, which induces a ``move'' effect on variable @x@, and thus disables any future use of all the variables aliased with @x@, while returning @x@ itself under a fresh qualifier.
\begin{lstlisting}
val x = ref 1; val y = x
val z = move(x)  // Ref[Int]$\trackvar{z}$  @mv(x) in context [z: Ref[Int]$\track$, y: Ref[Int]$\trackvar{x}$, x: Ref[Int]$\trackfresh$]
!x + !y          // type errors
\end{lstlisting}
After the $\tmove$ expression, variable @z@ is the
unique variable that can be used to access to the referent of @x@, and variables @x@ and @y@ have become inaccessible.

\subsection{Effect Inference/Checking}
\begin{figure*}[t]\small
\begin{mdframed}
\judgement{Effect Inference Rules}{\fbox{$\G[\algout{\flt}] \ts t \chek \ty{Q} \, \EPS \; | \; \MV $}
\fbox{$\G[\algout{\flt}] \ts t \chek \ty[\synth \algout{q}]{T} \, \EPS \; | \; \MV$}
\fbox{$\G[\algout{\flt}] \ts t \synth \algout{\ty{Q}} \, \EPS \; | \; \MV $}}\vspace{0ex}
\begin{minipage}[t]{.44\linewidth}\vspace{4pt}
\infrule[e-move]{
\G[\algout{\flt}] \ts t \synth \algout{\ty[q]{(\TRef~ \ty{B})}} \;  \EPS \; | \; \MV \\
\MV \sep q \\
\G[\algout{\flt}] \ts \tmove(t) \synth \algout{\ty[\qbot]{(\TRef~ \ty{B})}} \; \EPS \; | \; \MV \MVSEQ \MFX{q_{\setminus \QFresh}}
\vgap
\infrule[e-deref]{
\G[\algout{\flt}]\ts t \synth \algout{\ty[q]{(\TRef~\ty{B})}} \;  \EPS \; | \; \MV \quad
\MV \sep q
\G[\algout{\flt}]\ts !t \synth \algout{\ty[\qbot]{B}} \;  \EPS \EFFSEQ\FX{q_{\setminus \QFresh}} \; | \; \MV
\vgap
\infrule[e-assgn]{
\G[\algout{\flt_1}]\ts t_1 \synth \algout{\ty[q]{(\TRef~\ty{B})}} \;  \EPS[1] \; | \; \MV[1] \\
\G[\algout{\flt_2}]\ts t_2 \synth \algout{\ty[p]{B}} \;  \EPS[2] \; | \; \MV[2] \quad
\MV[1] \sep q  \\
\MV[1] \sep \EPS[2]  \quad
\MV[2] \sep q \quad \MV[1] \sep \MV[2]
\G[\algout{\flt_1,\flt_2}]\ts t_1 \coloneqq t_2 \synth \algout{\ty[\qbot]{B}} \EPS[1]\EFFSEQ\EPS[2]\EFFSEQ\FX{q_{\setminus \QFresh}} \; | \; \MV[1] \MVSEQ \MV[2]
\end{minipage}%
\begin{minipage}[t]{.03\linewidth}
\hspace{1pt}%
\end{minipage}%
\begin{minipage}[t]{.55\linewidth}\vspace{0pt}
\infrule[e-app]{
\G[\algout{\flt_1}]\ts t_1 \synth \algout{\ty[q]{\left(f(x: \ty[p]{T}) \stackrel{\EPS[3] \; | \; \MV[3]}{\longrightarrow} \ty[r]{U}\right)}} \; \EPS[1] \; | \; \MV[1] \\
\G[\algout{\flt_2}]\ts t_2 \chek \ty[\synth \algout{p'}]{T}\; \EPS[2] \; | \; \MV[2] \quad \quad \theta = [p'/x, q/f]\\
\left\{\begin{array}{l@{\ }l@{}}
\G[\algout{\flt'}]\ts p' < p, & \text{if~}\qfresh\notin p\land \lnot \textit{isVar}(t_1); \\[1ex]
\G[\algout{\flt'}]\ts p' < p_{[t_1/f]}, & \text{else if~}\qfresh\notin p\land \textit{isVar}(t_1);\\[1ex]
\begin{array}{@{}l}
\G[\algout{\flt'}]\ts p' \ll^p \algout{p''} \\[-.6ex]
\qquad \land ~{p''}_{\setminus p} \sep q,
\end{array} & \text{else if~}\qfresh\in p \land f\notin p; \\[2ex]
\algout{\flt'} = \qbot, & \text{otherwise}
\end{array}\right. \\
\algout{\flt} = \flt_1,\flt_2,\flt',r_{\setminus\starred{f,x}} \\
x \in \MV[3] \Rightarrow x \not\in r \quad
f \in \MV[3] \Rightarrow f \not\in r \quad
\MV[1] \sep \EPS[2] \\
\MV[1] \sep \MV[2] \sep \MV[3] \quad
(\MV[1], \MV[2]) \sep (p', q, \EPS[3])
\G[\algout{\flt}]\ts t_1~t_2 \synth \algout{\ty[r \theta]{U}} \, (\EPS[1] \EFFSEQ \EPS[2] \EFFSEQ \EPS[3] \; | \; \MV[1] \MVSEQ \MV[2] \MVSEQ \MV[3])\theta
\end{minipage}
\end{mdframed}
\caption{Selected effect inference rules.}
\label{fig:effects}
\vspace{-3ex}
\end{figure*}

\figref{fig:effects} shows selected effect inference rules,
which extend the bidirectional typing rules in \figref{fig:bidir} with inferred use effect (\EPS) and move effect (\MV) qualifiers.
The algorithm for checking sub-effects (omitted) follows the one for qualifiers in \figref{fig:algqual}.
Like reachability qualifiers, effects are finite sets of variables.
For simplicity we combine read/write effects into a single \textit{use effect}, denoting the set of variables that may be used during the computation.
A \textit{move effect} denotes the set of variables that may be moved (become inaccessible).
Function types carry effect qualifiers $\EPS \; | \; \MV$ for their latent effect.
In the figure, we write $\MV[1] \sep \MV[2] \sep \MV[3]$ as shorthand for mutual separation.

The effect of a compound term is the composition of the effects of each sub-term.
\citet{DBLP:journals/pacmpl/BaoWBJHR21} define a generic effect quantale~\cite{DBLP:journals/toplas/Gordon21}
parameterized with effect labels, which can be instantiated
in different ways to dictate the effect composition rules.
Here, we choose a more direct formalization, resulting in a more uniform system.
Dereferencing and updating a reference with type $\ty[q]{(\TRef~\ty{B})}$ induce a use effect on $q$ (rules \textsc{e-deref} and \textsc{e-assgn} respectively).

Composing use effects computes the least upper bound of them. %
Composing move effects takes a program's execution order into the account, and ensures that values cannot be reached from inaccessible  variables. %
Rule \textsc{e-move} makes variables in $q$ inaccessible, resulting in a tracked reference that can no longer be accessed through any variables.
An assignment (rule \textsc{e-assgn}) evaluates term $t_1$ followed by $t_2$; the latter
induces a use effect on variables in $\EPS[2]$, thus those variables must not be moved by $t_1$, \ie, $\MV[1]$ and $\EPS[2]$ are separate.
The last step of an assignment induces a use effect on accessible variables in $q$, thus $q$ must be separate from $\MV[1]$ and $\MV[2]$, which are moved by $t_1$ and $t_2$.
Function application (rule \textsc{e-app}) also checks that no inaccessible variables are returned. %

\subsection{Dependency Synthesis}\label{sec:dependency}
\citet{oopsla23,oopsla23supplement} have presented a dependency analysis on top of a reachability type-and-effect system~\cite{DBLP:journals/pacmpl/BaoWBJHR21} as the
basis for advanced compiler optimizations. However, their work assumes the non-algorithmic typing rules,
leaving open the question of decidable checking and inference, which is addressed in this work.
In this section, we discuss an end-to-end dependency analysis enabling safe dead-code elimination (DCE) using the following example:
\[
\setlength{\abovedisplayskip}{0pt}
\setlength{\belowdisplayskip}{0pt}
(\lambda ~ x.
(\lambda  ~y .
(\lambda~ z.
(\lambda~ m. y)(y := 2))
(x := 1)
\]
The code allocates a reference, passes it to the outer $\lambda$, updates it twice with a different variable name in the inner $\lambda$s and finally returns the reference.
The code is type-checked using the bidirectional typing algorithm (\eg,  by rules \textsc{ta-let}, \textsc{ta-ref} and \textsc{ta-assgn} in \figref{fig:bidir}).
To enable fine-grained dependency tracking, we assume the effect inference rules (in \figref{fig:effects}) are refined by splitting use effects into read and write effects,
and extend the effect system with the distinguished variable $\omega$ for allocating memory resources (following \citet{oopsla23,oopsla23supplement}).
With the refined and extended effect inference rules, we can infer that @ref(0)@ incudes a read effect on $\omega$, and the two assignments induce a write effect on @x@ and @y@ respectively.

Now, we use standard techniques to give names to subexpressions by inserting $\tlet$-bindings~\cite{DBLP:books/daglib/0005958},
and further translate the resulting program into the one below on the left, which is in A-normal form (ANF),\footnote{\citet{oopsla23,oopsla23supplement}'s work uses monadic normal form (MNF), which generalizes ANF by allowing nested let-bindings, for a simpler technical treatment of proving the meta-theory. The choice of MNF or ANF is irrelevant to our example.} where each block ends with a result variable.
Note that those steps are type-and-effect preserving~\cite{oopsla23,oopsla23supplement}.

\begin{minipage}{.62\textwidth}
\begin{lstlisting}
let x = ref 0         // Ref[Int]$\trackvar{\QFresh}$ @rd($\omega$) @wr($\PURE$)
let y  = x            // Ref[Int]$\trackvar{x}$ @rd($\PURE$) @wr($\PURE$)
let z = (x := 1)      // Unit$\trackl$      @rd($\PURE$) @wr{x}
let m = (y := 2)      // Unit$\trackl$      @rd($\PURE$) @wr{y}
y                     // Ref[Int]$\trackvar{x}$ @rd($\PURE$) @wr($\PURE$)
\end{lstlisting}
\end{minipage}%
\begin{minipage}{.4\textwidth}
\vspace{-12pt}
\begin{adjustbox}{scale=.7}\hspace{120pt}
\begin{tikzcd}[row sep=normal,column sep=normal,every matrix/.append style={nodes=expnode}]
|[alias=dummy,dummynode,nmute]|\ldots  & |[alias=x1]| \mathtt{x} \\
& |[alias=x2]| \mathtt{y} \\
& |[alias=x3]| \mathtt{z} \\
& |[alias=x4]| \mathtt{m}
\arrow[hardd,from=x1,to=dummy,"\omega",nmute]
\arrow[softd,from=x3,to=x1,bend right=60]{}{\mathtt{x}}
\arrow[softd,from=x4,to=x3,bend left=40]{}{\mathtt{x}}
\arrow[softd,from=x4,to=x3,bend right=40,"\mathtt{y}"']
\arrow[datad,from=x2,to=x1]
\arrow[datad,from=x3,to=x1,bend left=60]
\arrow[datad,from=x4,to=x2,bend left=80,crossing over]
\end{tikzcd}
\end{adjustbox}
\end{minipage}%

The program can also be viewed as a graph (above on the right), where $\tlet$ bindings denote named nodes, and variable occurrences indicate edges for data dependencies.
The graph is also connected with \mute{teal} edges denoting store dependencies synthesized by the algorithm in \citet{oopsla23,oopsla23supplement}'s work.
For example, the direct dashed edge (in \mute{teal}) from @m@ to @z@, labeled with @x@ and @y@, represents a \textit{soft dependency},
meaning that the computation on node @m@ uses the store location that may be reachable from variables @x@ and @y@,
where node @z@ is the last node where the location is written to.
The directed solid edge (in \mute{teal}) from $x$ to ``$\cdots$'', labeled with $\omega$, represents a \textit{hard dependency},
meaning that the computation on the node @x@ uses the store allocator $\omega$,
where all its prior uses are subsumed under ``$\dots$''.
The dependency of the result variable @y@ summarizes the effect dependencies (omitted in the graph), including their last effectful use,
\eg, the dependency on @x@ and @y@ at node<EMAIL_ADDRESS>The following snippet on the left shows the code with those synthesized store dependencies:

\vspace{-3pt}
\begin{minipage}{.5\textwidth}
\begin{lstlisting}
let x = ref 0      $\has$ {$\color{depmap}\omega$ ↦ ...}ₕ {}ₛ
let y = x          $\has$ {}ₕ {}ₛ
let z = (x := 1)   $\has$ {}ₕ {x ↦ x}ₛ
let m = (y := 2)   $\has$ {}ₕ {x ↦ z, y ↦ z}ₛ
y                  $\has$ {}ₕ {x ↦ m, y ↦ m}ₛ
\end{lstlisting}
\end{minipage}%
\begin{minipage}[t]{.02\linewidth}
\hspace{1pt}%
\end{minipage}%
\begin{minipage}{.5\textwidth}
\begin{lstlisting}
let x = ref 0      $\has$ {$\color{depmap}\omega$ ↦ ...}ₕ {}ₛ
let y = x          $\has$ {}ₕ {}ₛ

let m = (y := 2)   $\has$ {}ₕ {x ↦ x, y ↦ x}ₛ
y                  $\has$ {}ₕ {x ↦ m, y ↦ m}ₛ
\end{lstlisting}
\end{minipage}\\
With those store-dependencies, the node @z@ can be soundly removed by applying the equational rule for DCE,
as the subsequent computation does not have a data or had dependency on it.
After DCE, the dependencies will be mechanically re-wired as shown in the above code on the right (see \citet{oopsla23,oopsla23supplement}'s work for all the details).

\subsection{Polymorphic Effect Inference/Checking}
Reachability types support a precise notion of lightweight qualifier polymorphism~\cite{DBLP:journals/pacmpl/WeiBJBR24},
however, effect-polymorphic function types need additional work. Consider the following code:
\begin{lstlisting}
let x = ref 0
def f (g: (Int =>$\trackvarl{@mv(g)}$ Unit)$\trackfresh$) = { g(!x)  }     // @mv(g) @rd(x)
let y = ref 1; let z = ref 1               // actual typing:         desired typing:
f({ p => !move(y) + p })                   // @mv(y) @rd(x)          @mv(y) @rd(x)
f({ p => !z + p })                         // @mv(z) @rd(x)          @rd(z) @rd(x)
!z                                         // type error             type checks
\end{lstlisting}
Here, we want function @f@ to be as liberal as possible, accepting a function parameter @g@ with arbitrary latent effect, including the destructive move effect
(the top of the effect lattice~\cite{DBLP:journals/pacmpl/BaoWBJHR21})
on any of its captured variables.
To express this, we use a \emph{self-reference for effects}, \ie, @mv(g)@, as @g@'s latent
effect, indicating that it may induce a move effect on anything function @g@ captures,
according to the semantics of self-references.
In the code above, the overall effects of the two invocations of @f@ are resolved by substituting @g@ with @y@ and @z@ respectively,
resulting in move effects on them as shown above.
Thus, a type error occurs on the final expression @!z@, as variable @z@ is
no longer accessible.
However, this is not quite what we want.
We would expect the effect of the second invocation to be resolved as read effect
on @z@, which is the effect the argument closure actually induces.

\bfparagraph{Parametric Effect Polymorphism}

This situation requires some support for \emph{polymorphic} effects.
It is possible to add effect abstraction and effect variables to $\polylang{}$,
as in \citet{DBLP:journals/pacmpl/WeiBJBR24}'s work that
adds type and qualifiers abstraction.
However, a proliferation of effect variables severly inhibits the usability of
effect systems~\cite{DBLP:phd/ch/Rytz14} and also poses challenges for
effective type inference~\cite{DBLP:books/daglib/0005958}.
Fortunately, alternatives exists in the form of \emph{dependent} effects,
which lead to a form of effect polymorphism that is lightweight yet has a
high degree of precision.

\bfparagraph{Call-Dependent Effects}
Leveraging our bidirectional typing algorithm,
we can use function call syntax in effect qualifiers, alleviating the annotation overhead caused by using abstract effect variables.
Consider the revised function declaration:
\begin{lstlisting}
def f (g: (Int =>$\trackvarl{@mv(g)}$ Unit)$\trackfresh$) = { g(!x)  }     // @g() @rd(x)
\end{lstlisting}
Now function @f@'s latent effect uses @g()@, which is a \emph{call-dependent effect}.
This means that the effect depends on @g@'s effect when it is applied.
In general, if @g@ were applied to an argument with non-trivial qualifiers, the
effect would be<EMAIL_ADDRESS>Here, we use just @g()@ as the argument qualifier is empty.
In the example above, the overall effects of the two invocations are resolved by substituting their arguments' latent effect, not their captured variables,
gaining the desired precision. As a result, the final @!z@ type-checks.
The notion of call-dependent effects coincides with the idea of relative effects
The approach provides a lightweight form of effect polymorphism, eliminating
the need for additional effect parameters in higher-order functions, and has been experimentally validated in an effect checker for Scala~\cite{DBLP:phd/ch/Rytz14}.

\section{Related Work} \label{sec:related}

\paragraph{Tracking Reachability/Capturing in Types}
This work is closely related to the original development of reachability types
\cite{DBLP:journals/pacmpl/BaoWBJHR21} and its polymorphic variant
\cite{DBLP:journals/pacmpl/WeiBJBR24},
both of which have borrowed ideas from separation
This paper builds on top of the \citet{DBLP:journals/pacmpl/WeiBJBR24}'s
$\lambda^{\vardiamondsuit}$-calculus but
improves its key limitations by refining the subtyping relation with
self-references and developing a practical type checking algorithm.
The $\maybelang$-calculus in this work is monomorphic, but already
has a lightweight form a reachability polymorphism via dependent application.
Nevertheless, $\maybelang$ can be extended with quantified polymorphism a la
\citet{DBLP:journals/pacmpl/WeiBJBR24}.

Closely related, capturing types \cite{DBLP:journals/toplas/BoruchGruszeckiOLLB23,xuDegreesSeparationFlexible2023}
are an ongoing work to integrate escape checking and separation tracking of
capabilities into Scala 3.  Capturing types borrow ideas from modal type theory
\cite{DBLP:journals/tocl/NanevskiPP08} and deploy boxing and unboxing to
achieve capture tunneling with polymorphism.
Due to the lack of self-references, capturing types would be less
expressiveness in the case of tracking freshness, especially for non-scoped
introduction forms and escaping closures.

\paragraph{From Ownership to Reachability}

Ownership type systems~\cite{noble1998flexible,DBLP:conf/oopsla/ClarkePN98,DBLP:series/lncs/ClarkeOSW13,DBLP:conf/oopsla/PotaninNCB06}
control the access paths to objects and enforce strict heap invariants.
They can track sophisticated properties, but require considerable annotation
overhead, inhibiting their practical adoption.
Automatic ownership type inference tools~\cite{DBLP:conf/ecoop/DietlEM11, DBLP:conf/ecoop/HuangDME12} require heuristics or interaction from the programmer to achieve preferable
Rust~\cite{DBLP:conf/sigada/MatsakisK14,jung2021safe} takes a strong ownership model, enforcing that a mutable reference has to be unique, and a read-only reference may be shared.
It has been widely used in low-level systems programming.
Aiming at introducing Rust-style ownership types into functional languages,
this work and prior work in reachability types relax the ``shared XOR mutable''
restriction from Rust and track sharing (thus separation) in the presence of higher-order functions.
Uniqueness properties in reachability type systems can be enforced via move effects (see~\Cref{sec:exten}).

\paragraph{The Avoidance Problem}
Systems with dependent types often encounter \emph{the avoidance problem}:
there is no minimal typing to avoid mentioning a (type) variable,
which can occur in systems with bounded existential types \cite{DBLP:journals/tcs/GhelliP98}
or ML-style modules.
Due to the avoidance issue, some design of ML-style module systems lacks complete type
checking \cite{DBLP:journals/jfp/Leroy00}.
Refined designs of modules avoid the avoidance problem by elaborating types
with escaped variables into implicit existential types
\cite{DBLP:conf/popl/DreyerCH03,DBLP:journals/jfp/RossbergRD14}.
It is worth noting that the avoidance problem does not arise in systems with
full dependent types, since substitution there is unrestricted, as opposed to
systems where variables can only be substituted with other variables, such as
DOT \cite{DBLP:conf/oopsla/RompfA16}.
In this work, the escaping of variables is a similar instance of
the avoidance problem, where our solution, the self-reference, plays a similar
role to implicit existential types used in ML-style module systems.
However, self-references are not existential types, as they do not require
packing/unpacking and can be smoothly introduced via subtyping.
Also, regarding the semantics (cf. \Cref{sec2:bounds}),
self-references are different from the common subtyping rules for bounded
existential types \cite{DBLP:journals/ngc/WehrT11}.

\paragraph{Self-References are not Recursive Types}
While we borrow the $\mu$-notation for self-references (e.g., in \Cref{fig:counter}),
there are key differences between self-references and recursive types
\cite{DBLP:journals/toplas/AmadioC93}.
While both allow a construct to refer to itself, self-references refer to terms, not types. %
Moreover, qualifiers are always finite sets and not recursive.
In the pair example from \Cref{fig:counter}, we cannot recursively expand
the self-reference as one would do with recursive types.
In this regard, the interaction between self-reference subtyping and bounded
quantification should not be subtle as recursive types are \cite{DBLP:journals/pacmpl/ZhouZO23}.
We leave the extension of reachability types with recursive types as future work.

\paragraph{Type Inference with Subtyping} %
The Hindley-Milner (HM) typing algorithm \cite{DBLP:conf/popl/DamasM82}
is able to infer the most general type in polymorphic languages without subtyping.
HM(X) \cite{DBLP:journals/tapos/OderskySW99} extends HM to constrained types
including subtyping and it supports principal types.
Aiming for compactness, recent more sophisticated approaches
\cite{DBLP:journals/pacmpl/Parreaux20,DBLP:conf/popl/DolanM17} could infer
principal types in the presence of subtyping.

As opposed to global inference algorithms, bidirectional typing
\cite{DBLP:journals/csur/DunfieldK21,DBLP:conf/popl/DunfieldP04}
features local reasoning at the cost of some explicit type annotations.
While bidirectional typing is well-developed,
our adaption for
$\maybelang$ is unique,
featuring a hybrid checking/synthesizing mode that is similar
to the refinement strengthening used in \citet{DBLP:conf/pldi/PolikarpovaKS16}.
Furthermore, since bidirectional typing is complete for System $F_{<:}$,
which is the substrate of \citet{DBLP:journals/pacmpl/WeiBJBR24}'s polymorphic
reachability type system,
it is possible to extend the algorithm for $\maybelang$ with polymorphism
using local constraint solving~\cite{DBLP:journals/toplas/PierceT00,DBLP:conf/popl/OderskyZZ01}
or greedy instantiation~\cite{DBLP:conf/icfp/DunfieldK13,DBLP:journals/jfp/JonesVWS07}.

\section{Conclusion} \label{sec:conc}

In this work, we investigated self-references in reachability types,
enabling a higher degree of expressiveness compared with prior work.
We proposed the refined $\maybelang$-calculus with
position-aware subtyping and the notion of qualifier growth, allowing to derive
expressive subtype relations involving self-references.
We also developed a bidirectional typing algorithm for $\maybelang$,
making such a new design practical and implementable.
We examined the expressiveness of the language and the effectiveness of the algorithm
with a case study on Church-encoded pairs.
By developing $\maybelang$, its typing algorithm, data structure encodings, as
well Coq mechanization and prototypes for the type checker and the effect
system, this work makes reachability types more practical and expressive.
\section*{Data-Availability Statement}
This work comes with Coq mechanization for
$\maybelang$ and its metatheory (in \Cref{sec:lang}),
the bidirectional typing algorithm and its metatheory (in \Cref{sec:algo}),
and the examples in the case study (in \Cref{sec:encode}).
Supporting the main claims of this work, they will be available for artifact
Beyond the mechanization, there are also prototypes for
a type checker with System $F_{<:}$-style polymorphism (in \Cref{sec:poly})
and a graph IR codegen with flow-sensitive effect system (in \Cref{sec:exten}).
\begin{acks}                            %
We thank Haotian Deng for related contributions to reachability types,
and Zhe Zhou, Yongwei Yuan, and Patrick LaFontaine for feedbacks on early drafts.
We also thank the anonymous reviewers for their insightful comments and suggestions, as well as our generous funding providers.
\end{acks}

%%% -*-BibTeX-*-
%%% Do NOT edit. File created by BibTeX with style
%%% ACM-Reference-Format-Journals [18-Jan-2012].

\newcommand{\noop}[1]{}
\begin{thebibliography}{49}

%%% ====================================================================
%%% NOTE TO THE USER: you can override these defaults by providing
%%% customized versions of any of these macros before the \bibliography
%%% command.  Each of them MUST provide its own final punctuation,
%%% except for \shownote{}, \showDOI{}, and \showURL{}.  The latter two
%%% do not use final punctuation, in order to avoid confusing it with
%%% the Web address.
%%% To suppress output of a particular field, define its macro to expand
%%% to an empty string, or better, \unskip, like this:
%%% \newcommand{\showDOI}[1]{\unskip}   % LaTeX syntax
%%% \def \showDOI #1{\unskip}           % plain TeX syntax
%%% ====================================================================

\ifx \showCODEN    \undefined \def \showCODEN     #1{\unskip}     \fi
\ifx \showDOI      \undefined \def \showDOI       #1{#1}\fi
\ifx \showISBNx    \undefined \def \showISBNx     #1{\unskip}     \fi
\ifx \showISBNxiii \undefined \def \showISBNxiii  #1{\unskip}     \fi
\ifx \showISSN     \undefined \def \showISSN      #1{\unskip}     \fi
\ifx \showLCCN     \undefined \def \showLCCN      #1{\unskip}     \fi
\ifx \shownote     \undefined \def \shownote      #1{#1}          \fi
\ifx \showarticletitle \undefined \def \showarticletitle #1{#1}   \fi
\ifx \showURL      \undefined \def \showURL       {\relax}        \fi
% The following commands are used for tagged output and should be
% invisible to TeX
\providecommand\bibfield[2]{#2}
\providecommand\bibinfo[2]{#2}
\providecommand\natexlab[1]{#1}
\providecommand\showeprint[2][]{arXiv:#2}

\bibitem[Amadio and Cardelli(1993)]%
\bibfield{author}{\bibinfo{person}{Roberto~M. Amadio} {and}
\bibinfo{person}{Luca Cardelli}.} \bibinfo{year}{1993}\natexlab{}.
\newblock \showarticletitle{Subtyping Recursive Types}.
\newblock \bibinfo{journal}{\emph{{ACM} Trans. Program. Lang. Syst.}}
\bibinfo{volume}{15}, \bibinfo{number}{4} (\bibinfo{year}{1993}),
\bibinfo{pages}{575--631}.
\newblock

\bibitem[Amin et~al\mbox{.}(2016)]%
\bibfield{author}{\bibinfo{person}{Nada Amin}, \bibinfo{person}{Samuel
Gr{\"{u}}tter}, \bibinfo{person}{Martin Odersky}, \bibinfo{person}{Tiark
Rompf}, {and} \bibinfo{person}{Sandro Stucki}.}
\bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{The Essence of Dependent Object Types}. In
\bibinfo{booktitle}{\emph{A List of Successes That Can Change the World}}
\emph{(\bibinfo{series}{Lecture Notes in Computer Science},
Vol.~\bibinfo{volume}{9600})}. \bibinfo{publisher}{Springer},
\bibinfo{pages}{249--272}.
\newblock

\bibitem[Bao et~al\mbox{.}(2023)]%
\bibfield{author}{\bibinfo{person}{Yuyan Bao}, \bibinfo{person}{Guannan Wei},
\bibinfo{person}{Oliver Bra{\v c}evac}, {and} \bibinfo{person}{Tiark Rompf}.}
\bibinfo{year}{2023}\natexlab{}.
\newblock \showarticletitle{Modeling {{Reachability Types}} with {{Logical
\newblock  (\bibinfo{year}{2023}).
\newblock
\urldef\tempurl%
\url{https://doi.org/10.48550/ARXIV.2309.05885}
\showDOI{\tempurl}

\bibitem[Bao et~al\mbox{.}(2021)]%
\bibfield{author}{\bibinfo{person}{Yuyan Bao}, \bibinfo{person}{Guannan Wei},
\bibinfo{person}{Oliver Bra\v{c}evac}, \bibinfo{person}{Yuxuan Jiang},
\bibinfo{person}{Qiyang He}, {and} \bibinfo{person}{Tiark Rompf}.}
\bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Reachability types: tracking aliasing and
separation in higher-order functional programs}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{5}, \bibinfo{number}{{OOPSLA}} (\bibinfo{year}{2021}),
\bibinfo{pages}{1--32}.
\newblock

\bibitem[Boruch{-}Gruszecki et~al\mbox{.}(2023)]%
\bibfield{author}{\bibinfo{person}{Aleksander Boruch{-}Gruszecki},
\bibinfo{person}{Martin Odersky}, \bibinfo{person}{Edward Lee},
\bibinfo{person}{Ondrej Lhot{\'{a}}k}, {and}
\bibinfo{person}{Jonathan~Immanuel Brachth{\"{a}}user}.}
\bibinfo{year}{2023}\natexlab{}.
\newblock \showarticletitle{Capturing Types}.
\newblock \bibinfo{journal}{\emph{{ACM} Trans. Program. Lang. Syst.}}
\bibinfo{volume}{45}, \bibinfo{number}{4} (\bibinfo{year}{2023}),
\bibinfo{pages}{21:1--21:52}.
\newblock

\bibitem[Bra\v{c}evac et~al\mbox{.}(2023a)]%
\bibfield{author}{\bibinfo{person}{Oliver Bra\v{c}evac},
\bibinfo{person}{Guannan Wei}, \bibinfo{person}{Songlin Jia},
\bibinfo{person}{Supun Abeysinghe}, \bibinfo{person}{Yuxuan Jiang},
\bibinfo{person}{Yuyan Bao}, {and} \bibinfo{person}{Tiark Rompf}.}
\bibinfo{year}{2023}\natexlab{a}.
\newblock \showarticletitle{Graph IRs for Impure Higher-Order Languages: Making
Aggressive Optimizations Affordable with Precise Effect Dependencies}.
\newblock \bibinfo{journal}{\emph{Proc. ACM Program. Lang.}}
\bibinfo{volume}{7}, \bibinfo{number}{OOPSLA2}, Article
\bibinfo{articleno}{236} (\bibinfo{date}{oct} \bibinfo{year}{2023}),
\bibinfo{numpages}{31}~pages.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/3622813}
\showDOI{\tempurl}

\bibitem[Bra\v{c}evac et~al\mbox{.}(2023b)]%
\bibfield{author}{\bibinfo{person}{Oliver Bra\v{c}evac},
\bibinfo{person}{Guannan Wei}, \bibinfo{person}{Songlin Jia},
\bibinfo{person}{Supun Abeysinghe}, \bibinfo{person}{Yuxuan Jiang},
\bibinfo{person}{Yuyan Bao}, {and} \bibinfo{person}{Tiark Rompf}.}
\bibinfo{year}{2023}\natexlab{b}.
\newblock \bibinfo{title}{Graph IRs for Impure Higher-Order Languages
\newblock \bibinfo{howpublished}{arXiv preprint}.
\newblock

\bibitem[Cardelli(1993)]%
\bibfield{author}{\bibinfo{person}{Luca Cardelli}.}
\bibinfo{year}{1993}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{An implementation of F}}.
\newblock \bibinfo{publisher}{Digital Equipment Corporation Systems Research
\newblock

\bibitem[Clarke et~al\mbox{.}(2013)]%
\bibfield{author}{\bibinfo{person}{Dave Clarke}, \bibinfo{person}{Johan
{\"{O}}stlund}, \bibinfo{person}{Ilya Sergey}, {and} \bibinfo{person}{Tobias
Wrigstad}.} \bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Ownership Types: {A} Survey}.
\newblock In \bibinfo{booktitle}{\emph{Aliasing in Object-Oriented
Programming}}. \bibinfo{series}{Lecture Notes in Computer Science},
Vol.~\bibinfo{volume}{7850}. \bibinfo{publisher}{Springer},
\bibinfo{pages}{15--58}.
\newblock

\bibitem[Clarke et~al\mbox{.}(1998)]%
\bibfield{author}{\bibinfo{person}{David Clarke}, \bibinfo{person}{John
Potter}, {and} \bibinfo{person}{James Noble}.}
\bibinfo{year}{1998}\natexlab{}.
\newblock \showarticletitle{Ownership Types for Flexible Alias Protection}. In
\bibinfo{booktitle}{\emph{{OOPSLA}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{48--64}.
\newblock

\bibitem[Crary(2020)]%
\bibfield{author}{\bibinfo{person}{Karl Crary}.}
\bibinfo{year}{2020}\natexlab{}.
\newblock \showarticletitle{A focused solution to the avoidance problem}.
\newblock \bibinfo{journal}{\emph{J. Funct. Program.}}  \bibinfo{volume}{30}
(\bibinfo{year}{2020}), \bibinfo{pages}{e24}.
\newblock

\bibitem[Damas and Milner(1982)]%
\bibfield{author}{\bibinfo{person}{Lu{\'{\i}}s Damas} {and}
\bibinfo{person}{Robin Milner}.} \bibinfo{year}{1982}\natexlab{}.
\newblock \showarticletitle{Principal Type-Schemes for Functional Programs}. In
\bibinfo{booktitle}{\emph{{POPL}}}. \bibinfo{publisher}{{ACM} Press},
\bibinfo{pages}{207--212}.
\newblock

\bibitem[Dietl et~al\mbox{.}(2011)]%
\bibfield{author}{\bibinfo{person}{Werner Dietl}, \bibinfo{person}{Michael~D.
Ernst}, {and} \bibinfo{person}{Peter M{\"{u}}ller}.}
\bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{Tunable Static Inference for Generic Universe
Types}. In \bibinfo{booktitle}{\emph{{ECOOP}}}
\emph{(\bibinfo{series}{Lecture Notes in Computer Science},
Vol.~\bibinfo{volume}{6813})}. \bibinfo{publisher}{Springer},
\bibinfo{pages}{333--357}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-642-22655-7\_16}
\showDOI{\tempurl}

\bibitem[Dolan and Mycroft(2017)]%
\bibfield{author}{\bibinfo{person}{Stephen Dolan} {and} \bibinfo{person}{Alan
Mycroft}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{Polymorphism, subtyping, and type inference in
MLsub}. In \bibinfo{booktitle}{\emph{{POPL}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{60--72}.
\newblock

\bibitem[Dreyer et~al\mbox{.}(2003)]%
\bibfield{author}{\bibinfo{person}{Derek Dreyer}, \bibinfo{person}{Karl Crary},
{and} \bibinfo{person}{Robert Harper}.} \bibinfo{year}{2003}\natexlab{}.
\newblock \showarticletitle{A type system for higher-order modules}. In
\bibinfo{booktitle}{\emph{{POPL}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{236--249}.
\newblock

\bibitem[Dreyer et~al\mbox{.}(2005)]%
\bibfield{author}{\bibinfo{person}{Derek Dreyer}, \bibinfo{person}{Robert
Harper}, {and} \bibinfo{person}{Karl Crary}.}
\bibinfo{year}{2005}\natexlab{}.
\newblock \emph{\bibinfo{title}{Understanding and evolving the ml module
\newblock \bibinfo{thesistype}{Ph.\,D. Dissertation}. \bibinfo{address}{USA}.
\newblock
\showISBNx{0542015501}
\newblock
\shownote{AAI3166274}.

\bibitem[Dunfield and Krishnaswami(2022)]%
\bibfield{author}{\bibinfo{person}{Jana Dunfield} {and} \bibinfo{person}{Neel
Krishnaswami}.} \bibinfo{year}{2022}\natexlab{}.
\newblock \showarticletitle{Bidirectional Typing}.
\newblock \bibinfo{journal}{\emph{{ACM} Comput. Surv.}} \bibinfo{volume}{54},
\bibinfo{number}{5} (\bibinfo{year}{2022}), \bibinfo{pages}{98:1--98:38}.
\newblock

\bibitem[Dunfield and Krishnaswami(2013)]%
\bibfield{author}{\bibinfo{person}{Jana Dunfield} {and}
\bibinfo{person}{Neelakantan~R. Krishnaswami}.}
\bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{Complete and easy bidirectional typechecking for
higher-rank polymorphism}. In \bibinfo{booktitle}{\emph{{ICFP}}}.
\bibinfo{publisher}{{ACM}}, \bibinfo{pages}{429--442}.
\newblock

\bibitem[Dunfield and Pfenning(2004)]%
\bibfield{author}{\bibinfo{person}{Jana Dunfield} {and} \bibinfo{person}{Frank
Pfenning}.} \bibinfo{year}{2004}\natexlab{}.
\newblock \showarticletitle{Tridirectional typechecking}. In
\bibinfo{booktitle}{\emph{{POPL}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{281--292}.
\newblock

\bibitem[Ghelli and Pierce(1998)]%
\bibfield{author}{\bibinfo{person}{Giorgio Ghelli} {and}
\bibinfo{person}{Benjamin~C. Pierce}.} \bibinfo{year}{1998}\natexlab{}.
\newblock \showarticletitle{Bounded Existentials and Minimal Typing}.
\newblock \bibinfo{journal}{\emph{Theor. Comput. Sci.}} \bibinfo{volume}{193},
\bibinfo{number}{1-2} (\bibinfo{year}{1998}), \bibinfo{pages}{75--96}.
\newblock

\bibitem[Gordon(2021)]%
\bibfield{author}{\bibinfo{person}{Colin~S. Gordon}.}
\bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Polymorphic Iterable Sequential Effect Systems}.
\newblock \bibinfo{journal}{\emph{{ACM} Trans. Program. Lang. Syst.}}
\bibinfo{volume}{43}, \bibinfo{number}{1} (\bibinfo{year}{2021}),
\bibinfo{pages}{4:1--4:79}.
\newblock

\bibitem[Huang et~al\mbox{.}(2012)]%
\bibfield{author}{\bibinfo{person}{Wei Huang}, \bibinfo{person}{Werner Dietl},
\bibinfo{person}{Ana~L. Milanova}, {and} \bibinfo{person}{Michael~D. Ernst}.}
\bibinfo{year}{2012}\natexlab{}.
\newblock \showarticletitle{Inference and Checking of Object Ownership}. In
\bibinfo{booktitle}{\emph{{ECOOP}}} \emph{(\bibinfo{series}{Lecture Notes in
Computer Science}, Vol.~\bibinfo{volume}{7313})}.
\bibinfo{publisher}{Springer}, \bibinfo{pages}{181--206}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/978-3-642-31057-7\_9}
\showDOI{\tempurl}

\bibitem[Jones et~al\mbox{.}(2007)]%
\bibfield{author}{\bibinfo{person}{Simon L.~Peyton Jones},
\bibinfo{person}{Dimitrios Vytiniotis}, \bibinfo{person}{Stephanie Weirich},
{and} \bibinfo{person}{Mark Shields}.} \bibinfo{year}{2007}\natexlab{}.
\newblock \showarticletitle{Practical type inference for arbitrary-rank types}.
\newblock \bibinfo{journal}{\emph{J. Funct. Program.}} \bibinfo{volume}{17},
\bibinfo{number}{1} (\bibinfo{year}{2007}), \bibinfo{pages}{1--82}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1017/S0956796806006034}
\showDOI{\tempurl}

\bibitem[Jung et~al\mbox{.}(2021)]%
\bibfield{author}{\bibinfo{person}{Ralf Jung}, \bibinfo{person}{Jacques-Henri
Jourdan}, \bibinfo{person}{Robbert Krebbers}, {and} \bibinfo{person}{Derek
Dreyer}.} \bibinfo{year}{2021}\natexlab{}.
\newblock \showarticletitle{Safe systems programming in Rust}.
\newblock \bibinfo{journal}{\emph{Commun. ACM}} \bibinfo{volume}{64},
\bibinfo{number}{4} (\bibinfo{year}{2021}), \bibinfo{pages}{144--152}.
\newblock

\bibitem[Leroy(2000)]%
\bibfield{author}{\bibinfo{person}{Xavier Leroy}.}
\bibinfo{year}{2000}\natexlab{}.
\newblock \showarticletitle{A modular module system}.
\newblock \bibinfo{journal}{\emph{J. Funct. Program.}} \bibinfo{volume}{10},
\bibinfo{number}{3} (\bibinfo{year}{2000}), \bibinfo{pages}{269--303}.
\newblock

\bibitem[Lillibridge(1996)]%
\bibfield{author}{\bibinfo{person}{Mark Lillibridge}.}
\bibinfo{year}{1996}\natexlab{}.
\newblock \emph{\bibinfo{title}{Translucent {{Sums}}: {{A Foundation}} for
{{Higher-Order Module Systems}}}}.
\newblock \bibinfo{thesistype}{Ph.\,D. Dissertation}.
\newblock

\bibitem[Matsakis and Klock(2014)]%
\bibfield{author}{\bibinfo{person}{Nicholas~D. Matsakis} {and}
\bibinfo{person}{Felix S.~II Klock}.} \bibinfo{year}{2014}\natexlab{}.
\newblock \showarticletitle{The {Rust} language}. In
\bibinfo{booktitle}{\emph{{HILT}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{103--104}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/2663171.2663188}
\showDOI{\tempurl}

\bibitem[Nanevski et~al\mbox{.}(2008)]%
\bibfield{author}{\bibinfo{person}{Aleksandar Nanevski}, \bibinfo{person}{Frank
Pfenning}, {and} \bibinfo{person}{Brigitte Pientka}.}
\bibinfo{year}{2008}\natexlab{}.
\newblock \showarticletitle{Contextual modal type theory}.
\newblock \bibinfo{journal}{\emph{{ACM} Trans. Comput. Log.}}
\bibinfo{volume}{9}, \bibinfo{number}{3} (\bibinfo{year}{2008}),
\bibinfo{pages}{23:1--23:49}.
\newblock

\bibitem[Noble et~al\mbox{.}(1998)]%
\bibfield{author}{\bibinfo{person}{James Noble}, \bibinfo{person}{Jan Vitek},
{and} \bibinfo{person}{John Potter}.} \bibinfo{year}{1998}\natexlab{}.
\newblock \showarticletitle{Flexible Alias Protection}. In
\bibinfo{booktitle}{\emph{{ECOOP}}} \emph{(\bibinfo{series}{Lecture Notes in
Computer Science}, Vol.~\bibinfo{volume}{1445})}.
\bibinfo{publisher}{Springer}, \bibinfo{pages}{158--185}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1007/BFb0054091}
\showDOI{\tempurl}

\bibitem[Odersky et~al\mbox{.}(1999)]%
\bibfield{author}{\bibinfo{person}{Martin Odersky}, \bibinfo{person}{Martin
Sulzmann}, {and} \bibinfo{person}{Martin Wehr}.}
\bibinfo{year}{1999}\natexlab{}.
\newblock \showarticletitle{Type Inference with Constrained Types}.
\newblock \bibinfo{journal}{\emph{Theory Pract. Object Syst.}}
\bibinfo{volume}{5}, \bibinfo{number}{1} (\bibinfo{year}{1999}),
\bibinfo{pages}{35--55}.
\newblock

\bibitem[Odersky et~al\mbox{.}(2001)]%
\bibfield{author}{\bibinfo{person}{Martin Odersky}, \bibinfo{person}{Christoph
Zenger}, {and} \bibinfo{person}{Matthias Zenger}.}
\bibinfo{year}{2001}\natexlab{}.
\newblock \showarticletitle{Colored local type inference}. In
\bibinfo{booktitle}{\emph{{POPL}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{41--53}.
\newblock

\bibitem[O'Hearn et~al\mbox{.}(2001)]%
\bibfield{author}{\bibinfo{person}{Peter~W. O'Hearn}, \bibinfo{person}{John~C.
Reynolds}, {and} \bibinfo{person}{Hongseok Yang}.}
\bibinfo{year}{2001}\natexlab{}.
\newblock \showarticletitle{Local Reasoning about Programs that Alter Data
Structures}. In \bibinfo{booktitle}{\emph{{CSL}}}
\emph{(\bibinfo{series}{Lecture Notes in Computer Science},
Vol.~\bibinfo{volume}{2142})}. \bibinfo{publisher}{Springer},
\bibinfo{pages}{1--19}.
\newblock

\bibitem[Parreaux(2020)]%
\bibfield{author}{\bibinfo{person}{Lionel Parreaux}.}
\bibinfo{year}{2020}\natexlab{}.
\newblock \showarticletitle{The simple essence of algebraic subtyping:
principal type inference with subtyping made easy (functional pearl)}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{4}, \bibinfo{number}{{ICFP}} (\bibinfo{year}{2020}),
\bibinfo{pages}{124:1--124:28}.
\newblock

\bibitem[Pierce(2002)]%
\bibfield{author}{\bibinfo{person}{Benjamin~C. Pierce}.}
\bibinfo{year}{2002}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{Types and programming languages}}.
\newblock \bibinfo{publisher}{{MIT} Press}.
\newblock

\bibitem[Pierce and Turner(2000)]%
\bibfield{author}{\bibinfo{person}{Benjamin~C. Pierce} {and}
\bibinfo{person}{David~N. Turner}.} \bibinfo{year}{2000}\natexlab{}.
\newblock \showarticletitle{Local type inference}.
\newblock \bibinfo{journal}{\emph{{ACM} Trans. Program. Lang. Syst.}}
\bibinfo{volume}{22}, \bibinfo{number}{1} (\bibinfo{year}{2000}),
\bibinfo{pages}{1--44}.
\newblock

\bibitem[Polikarpova et~al\mbox{.}(2016)]%
\bibfield{author}{\bibinfo{person}{Nadia Polikarpova}, \bibinfo{person}{Ivan
Kuraj}, {and} \bibinfo{person}{Armando Solar{-}Lezama}.}
\bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Program synthesis from polymorphic refinement
types}. In \bibinfo{booktitle}{\emph{{PLDI}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{522--538}.
\newblock

\bibitem[Potanin et~al\mbox{.}(2006)]%
\bibfield{author}{\bibinfo{person}{Alex Potanin}, \bibinfo{person}{James
Noble}, \bibinfo{person}{Dave Clarke}, {and} \bibinfo{person}{Robert
Biddle}.} \bibinfo{year}{2006}\natexlab{}.
\newblock \showarticletitle{Generic ownership for generic Java}. In
\bibinfo{booktitle}{\emph{{OOPSLA}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{311--324}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1145/1167473.1167500}
\showDOI{\tempurl}

\bibitem[Reynolds(2002)]%
\bibfield{author}{\bibinfo{person}{John~C. Reynolds}.}
\bibinfo{year}{2002}\natexlab{}.
\newblock \showarticletitle{Separation Logic: {A} Logic for Shared Mutable Data
Structures}. In \bibinfo{booktitle}{\emph{{LICS}}}.
\bibinfo{publisher}{{IEEE} Computer Society}, \bibinfo{pages}{55--74}.
\newblock

\bibitem[Rompf and Amin(2016)]%
\bibfield{author}{\bibinfo{person}{Tiark Rompf} {and} \bibinfo{person}{Nada
Amin}.} \bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Type soundness for dependent object types {(DOT)}}.
In \bibinfo{booktitle}{\emph{{OOPSLA}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{624--641}.
\newblock

\bibitem[Rossberg et~al\mbox{.}(2014)]%
\bibfield{author}{\bibinfo{person}{Andreas Rossberg},
\bibinfo{person}{Claudio~V. Russo}, {and} \bibinfo{person}{Derek Dreyer}.}
\bibinfo{year}{2014}\natexlab{}.
\newblock \showarticletitle{F-ing modules}.
\newblock \bibinfo{journal}{\emph{J. Funct. Program.}} \bibinfo{volume}{24},
\bibinfo{number}{5} (\bibinfo{year}{2014}), \bibinfo{pages}{529--607}.
\newblock

\bibitem[Rytz(2014)]%
\bibfield{author}{\bibinfo{person}{Lukas Rytz}.}
\bibinfo{year}{2014}\natexlab{}.
\newblock \emph{\bibinfo{title}{A Practical Effect System for Scala}}.
\newblock \bibinfo{thesistype}{Ph.\,D. Dissertation}. \bibinfo{school}{EPFL,
\newblock
\urldef\tempurl%
\url{https://doi.org/10.5075/EPFL-THESIS-5935}
\showDOI{\tempurl}

\bibitem[Rytz and Odersky(2012)]%
\bibfield{author}{\bibinfo{person}{Lukas Rytz} {and} \bibinfo{person}{Martin
Odersky}.} \bibinfo{year}{2012}\natexlab{}.
\newblock \showarticletitle{Relative Effect Declarations for Lightweight
\newblock  (\bibinfo{year}{2012}).
\newblock
\urldef\tempurl%
\url{http://infoscience.epfl.ch/record/175546}
\showURL{%
\tempurl}

\bibitem[Timany et~al\mbox{.}(2024)]%
\bibfield{author}{\bibinfo{person}{Amin Timany}, \bibinfo{person}{Robbert
Krebbers}, \bibinfo{person}{Derek Dreyer}, {and} \bibinfo{person}{Lars
Birkedal}.} \bibinfo{year}{2024}\natexlab{}.
\newblock \showarticletitle{A {{Logical Approach}} to {{Type Soundness}}}.
\newblock  (\bibinfo{year}{2024}).
\newblock

\bibitem[Tschantz and Ernst(2005)]%
\bibfield{author}{\bibinfo{person}{Matthew~S. Tschantz} {and}
\bibinfo{person}{Michael~D. Ernst}.} \bibinfo{year}{2005}\natexlab{}.
\newblock \showarticletitle{Javari: adding reference immutability to Java}. In
\bibinfo{booktitle}{\emph{{OOPSLA}}}. \bibinfo{publisher}{{ACM}},
\bibinfo{pages}{211--230}.
\newblock

\bibitem[Wehr and Thiemann(2011)]%
\bibfield{author}{\bibinfo{person}{Stefan Wehr} {and} \bibinfo{person}{Peter
Thiemann}.} \bibinfo{year}{2011}\natexlab{}.
\newblock \showarticletitle{On the Decidability of Subtyping with Bounded
Existential Types and Implementation Constraints}.
\newblock \bibinfo{journal}{\emph{New Gener. Comput.}} \bibinfo{volume}{29},
\bibinfo{number}{1} (\bibinfo{year}{2011}), \bibinfo{pages}{87--124}.
\newblock

\bibitem[Wei et~al\mbox{.}(2024)]%
\bibfield{author}{\bibinfo{person}{Guannan Wei}, \bibinfo{person}{Oliver
Bracevac}, \bibinfo{person}{Songlin Jia}, \bibinfo{person}{Yuyan Bao}, {and}
\bibinfo{person}{Tiark Rompf}.} \bibinfo{year}{2024}\natexlab{}.
\newblock \showarticletitle{Polymorphic Reachability Types: Tracking Freshness,
Aliasing, and Separation in Higher-Order Generic Programs}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}
\bibinfo{volume}{8}, \bibinfo{number}{{POPL}} (\bibinfo{year}{2024}),
\bibinfo{pages}{393--424}.
\newblock

\bibitem[Xu and Odersky(2023)]%
\bibfield{author}{\bibinfo{person}{Yichen Xu} {and} \bibinfo{person}{Martin
Odersky}.} \bibinfo{year}{2023}\natexlab{}.
\newblock \bibinfo{title}{Degrees of {{Separation}}: {{A Flexible Type System}}
for {{Data Race Prevention}}}.
\newblock
\newblock

\bibitem[Zhou et~al\mbox{.}(2023)]%
\bibfield{author}{\bibinfo{person}{Litao Zhou}, \bibinfo{person}{Yaoda Zhou},
{and} \bibinfo{person}{Bruno~C. d. S.~Oliveira}.}
\bibinfo{year}{2023}\natexlab{}.
\newblock \showarticletitle{Recursive Subtyping for All}.
\newblock \bibinfo{journal}{\emph{Proc. {ACM} Program. Lang.}}