is then transformed into something like *g* (+) *x y* = (*x* + *y*, *y* + *y*). Now, consider the case that we pass an H-value to x and an L-value to y; the operator (+) produces an L-value if and only if both arguments are L-values. Without higher-ranked annotations, the annotation on the first argument to (+) has to be consistent with all uses of (+). Because x is an H-value, that will then also be the case for the second call to (+), leading to a pair of values of which the components are both H-values. With higher-ranked annotations, we can instantiate the two instances independently, and the second component of the pair is analyzed to produce an L-value. Functions in Haskell that use type classes are extremely common.

#### **3 The** *λ-***-calculus**

An essential ingredient of our annotated type system is the language of annotations that we use to decorate our types and to represent the dependencies resulting from evaluating an expression. Indeed, the fact that annotations are in fact "programs" in a lambda calculus is what allows us to make our analysis a higher-ranked polyvariant one. For the purpose of this paper, we generalize the λ∪-calculus of [16] to the λ-calculus (λ for short) a simply typed lambda calculus extended with a lattice structure.

The syntax of λ is given in figure 1; from now on, we refer to its types exclusively as *sorts*. Here, κ ranges over sorts, β over annotation variables, etc. κ ∈ **AnnSort** ::= (base sort) | κ1 ⇒ κ2 (function sort) β ∈ **AnnVar** (annotation variables) ξ ∈ **AnnTm** ::= β (variable) | λβ :: κ.ξ (abstraction) | ξ1 ξ2 (application) | (lattice value, ∈ L) | ξ1 ξ2 (lattice join operation)

Fig. 1: The syntax of the λ-calculus, sorts and annotations

In order to avoid confusion with the field of (algebraic) effects, we refer to terms of λ as *dependency terms* or *dependency annotations*. Terms are either of base sort , representing values in the underlying lattice L, or of function sort κ1 ⇒ κ2.

On the term level, we allow arbitrary elements of the underlying lattice and taking binary joins, in addition to the usual variables, function applications and lambda abstractions. Lattice elements are assumed to be taken from a *bounded join-semilattice* L, an algebraic structure L, consisting of an underlying set L and an associative, commutative and idempotent binary operation , called *join* (we usually write ∈ L for ∈ L), and a least element ⊥.

The sorting rules of λ are straightforward (see [26]). Values of the underlying lattice are always of sort , and the join operator is defined on arbitrary terms of the same sort:

$$\begin{array}{c} \Sigma \vdash\_{\mathsf{s}} \xi\_{1} : \kappa \qquad \Sigma \vdash\_{\mathsf{s}} \xi\_{2} : \kappa \\ \hline \Sigma \vdash\_{\mathsf{s}} \xi\_{1} \sqcup \xi\_{2} : \kappa \end{array} [\mathsf{S}\text{-JonN}].$$

The sorting rule uses *sort environments* denoted by the letter Σ that map annotation variables β to sorts κ. We denote the set of sort environments by **SortEnv**. More precisely, a *sort environment* or *sort context* Σ is a finite list of bindings from annotation variables β to sorts κ. The empty context is written as ∅ (in code as []), and the context Σ extended with the binding of the variable

$$\begin{aligned} V\_{\star} &= \mathcal{L} \\ V\_{\kappa\_1 \mapsto \kappa\_2} &= \{ f : V\_{\kappa\_1} \to V\_{\kappa\_2} \mid f \text{ mono} \} \\ \rho : \mathbf{AnnVar} &\rightarrow \text{fin} \bigcup \{ V\_{\kappa} \mid \kappa \in \mathbf{AnnSort} \} \\ \left[ \mathbb{\hat{\beta}} \right]\_{\rho} &= \rho(\beta) \end{aligned}$$

$$\begin{aligned} \left[ \begin{aligned} \mathbb{\hat{\beta}} \boldsymbol{\beta} &: \kappa\_1 \boldsymbol{\xi} \right]\_{\rho} = \lambda v \in V\_{\kappa\_1} \dots \mathbb{\left[ \boldsymbol{\xi} \right]}\_{\rho \left[ \boldsymbol{\beta} \mapsto v \right]} \\ \left[ \mathbb{\boldsymbol{\xi}}\_1 \ \mathbb{\boldsymbol{\xi}} \right]\_{\rho} = \left[ \mathbb{\boldsymbol{\xi}}\_1 \right]\_{\rho} \left( \left[ \mathbb{\boldsymbol{\xi}} \boldsymbol{\xi} \right]\_{\rho} \right) \\ \left[ \mathbb{\boldsymbol{\xi}} \right]\_{\rho} = \boldsymbol{\ell} \\ \left[ \mathbb{\boldsymbol{\xi}}\_1 \ \mathbb{\boldsymbol{\xi}} \right]\_{\rho} = \left[ \mathbb{\boldsymbol{\xi}}\_1 \right]\_{\rho} \sqcup \left[ \mathbb{\boldsymbol{\xi}}\_2 \right]\_{\rho} \end{aligned} \right.$$

Fig. 2: The semantics of λ-calculus

β to the sort κ is written Σ,β : κ. We denote the set of annotation variables in the context Σ with dom(Σ). When we write, Σ(β) = κ this means that β ∈ dom(Σ) and the rightmost occurrence of β binds it to κ. Moreover, Σ \ B where B ⊆ **AnnVar** denotes the context Σ where all bindings of annotation variables in B have been removed. In the remainder of this paper, we shall overload this notation for all kinds of other environments we shall be needing, including type environments, and annotated type environments.

The λ-calculus enjoys a number of properties, many of which are what one might expect; we have put these and their proofs in [26].

A *substitution* is a map from variables to terms usually denoted by the letter θ. The application of a substitution θ to a term ξ is written θξ and replaces all free variables in ξ that are also in the domain of θ with the corresponding terms they are mapped to. A concrete substitution replacing the variables β1,...,βn with terms ξ1,...,ξn is written [ξ1/β1,...,ξn/βn].

Assuming the usual definitions for the pointwise extension of a lattice L, and for monotone (order-preserving) functions between lattices, Figure 2 shows the denotational semantics of λ, where we employ the pointwise lifting of ∪ to functions to give semantics to the join of λ. The universe Vκ denotes the lattice that is represented by the sort κ. The base sort represents the underlying lattice L and the function sort κ1 ⇒ κ2 represents the lattice constructed by pointwise extension of the lattice Vκ2 restricted to monotone functions.

The denotation function -·ρ is parameterized with an environment ρ of the given type that provides the values of variables. The denotation of a lambda term is simply an element of the corresponding function space. Applications are therefore mapped directly to the underlying function application of the metatheory. This is unlike the λ∪-calculus of [16] where lambda terms are mapped to singleton sets of functions and function application is defined in terms of the union of the results of individually applying each function. The crucial difference is that we have offloaded this complexity into the definition of the pointwise extension of lattices. It is therefore important to note that the join operator used in the denotation of a term ξ1 ξ2 depends on the sort κ of this term and belongs to the lattice Vκ.

An environment ρ : **AnnVar** →fin - {Vκ | κ ∈ **AnnSort**} and a sort environment Σ are *compatible* if dom(Σ) = dom(ρ) and for all β ∈ dom(Σ) we have ρ(β) ∈ VΣ(β). Given two dependency terms ξ1 and ξ2 and a sort κ such that Σ s ξ1 : κ and Σ s ξ2 : κ, we say that ξ2 *subsumes* ξ1 under the environment Σ, written Σ sub ξ1 ξ2, if for all environments ρ compatible with Σ, we have ξ1ρ ξ2ρ. They are *semantically equal* under Σ, written Σ ξ1 ≡ ξ2, if for all environments ρ compatible with Σ, we have ξ1ρ = ξ2ρ.

# **4 The declarative type system**

The types and syntax of our source language are given in figure 3. The types of our source language consist of a unit type, and product, sum and function types. As mentioned earlier, let-polymorphism at the type level is not part of the

Fig. 3: The types and terms of the source language

type system. The language itself is then hardly suprising and includes variables, a unit constant, lambda abstraction, function application, projection functions for product types, sum constructors, a sum eliminator (case), fixpoints, seq for explicitly forcing evaluation in our call-by-name language, and, finally, a special operation ann(*t*) that raises the annotation level of *t* to . We omit the underlying type system for the source language since it consists mostly of the standard rules (see [26]). A notable exception is the rule for ann(*t*). Such an explicitly annotated term has the same underlying type as *t*:

$$\frac{\Gamma \vdash t : \tau}{\Gamma \vdash \text{ann}\_{\ell}(t) : \tau} \text{ [U-ANN]};$$

The annotation imposed on t only becomes relevant in the annotated type system that we discuss next. In the following, we assume the usual definitions for computing the set of free term variables of a term, ftv(t).

**The annotated type system** The source language is simply a desugared variant of the functional language a programmer deals with. The target language has the same structure, but adds dependency annotations to the source syntax. These annotations are the payload of the dependency analaysis and computed by the algorithm given in section 6, so that the analysis results can be employed in the back-end of a compiler. In other words, the algorithm *elaborates* a source level term into a target term.

The syntax of the target language is shown in figure 4. *Annotated types* of the target language are denoted by τ and *annotated terms* are denoted by t. The annotations that we put on compound types, as well as their components are not just there for uniformity. Because of our non-strict semantics and the

Fig. 4: The annotated types and terms of the target language

presence of seq, we can observe the effects on a pair constructor independently of its values, so we have separate annotations to represent these.

On the type level, there is an additional construct ∀β :: κ.τ quantifying over an annotation variable β of sort κ. Furthermore, the recursive occurrences in the sum, product and arrow types now each carry an annotation. On the term level, the explicit type annotations of lambda expressions and fixpoints are now annotated types and also include a dependency annotation. Moreover, dependency abstraction and application have been added to reflect the quantification of dependency variables on the type level. We denote the set of free (term) variables in a target term *t* by ftv(*t*).

The formal definition of well-formedness for annotated types can be found in [26]. Informally, a type is well-formed only if all annotations are of sort and all annotation variables that are used have previously been bound.

Below, we assume the unsurprising recursive definitions for computing the underlying terms *t* and underlying types τ that correspond to annotated terms *t* and annotated types τ. We also straightforwardly extend the definition of free annotation variables to annotated types, and denote these by fav(τ).

**Subtyping** To define subtyping we need an auxiliary relation that says when two annotated types τ1 and τ2 *have the same shape*. The unsurprising formal definition is in [26], but essentially they have the same syntactic structure, and in the forall case, quantify over the same annotation variable. It can be quite easily proven that if two types have the same shape, then they have the same underlying type. This is not true the other way around: the annotated types ∀β1.∀β2.intβ1 → intβ1 β2 and ∀β1.intβ1 → intβ1 have the same underlying type, int → int, but do not have the same shape.

Figure 5 shows the rules defining the subtyping relation on annotated types of the same shape, that allows us to weaken the annotations on a type to a less demanding one.  The subtyping relation only relates the annotations inside the types using the subsumption relation Σ sub ξ1 ξ2 between dependency terms. Moreover, the subtyping relation implicitly demands that both types are well-formed under the environment. The [Sub-Forall] rule requires that the quantified variable has the same name in both types. This is not a restriction, as we can simply rename the variables in one or both of the types accordingly in order to make them match and prevent unintentional capturing of previously free variables. Note that [Sub-Arr] is contravariant for argument positions. We omitted [Sub-Sum] which can be derived from [Sub-Prod] by replacing × with +.

**The annotated type rules** An *annotated type environment* Γ is defined analogously to sort environments, but instead maps term variables x to pairs of an annotated type τ and a dependency term ξ. We extend the definition of the set of free annotation variables to annotated environments by taking the union of the free annotation variables of all annotated types and dependency terms occurring in the environment, denoted by fav(Γ). We denote the set of annotated type environments by **AnnTyEnv**.

We have now all the definitions in place in order to define the declarative annotated type system shown in figure 6. It consists of judgments of the form Σ | Γ te t : τ & ξ expressing that under the sort environment Σ and the annotated type environment Γ, the annotated term t has the annotated type τ and the dependency term ξ. The dependency term in this context is also called the *dependency term* of t 1. It is implicitly assumed that every type τ is also wellformed under Σ, i.e. Σ wft τ, and that the resulting dependency annotation ξ is of sort , i.e. Σ s ξ : .

We now discuss some of the more interesting rules of figure 6. In [T-Var], both the annotated type and the dependency annotation are looked up in the environment. The dependency annotation of the unit value defaults to the least annotation in [T-Unit]. While we could admit an arbitrary dependency annotation here, the same can be achieved by using the subtyping rule [T-Sub]. We employ this principle more often, e.g., in [T-Abs], and [T-Pair]. This essentially means that the context in which such a term is used completely determines the annotation.

The rule [T-App] may seem overly restrictive by requiring that the types and dependency annotations of the arguments match, and that the dependency annotations of the return value and the function itself are the same. However, in combination with the subtyping rule [T-Sub], this effectively does not restrict the analysis in any way. We see the same happening in other rules, such as [T-Case] and [T-Proj]. Note that the dependency annotation of the argument does not play a role in the resulting dependency annotation of the application. This is because we are dealing with a call by name semantics which means that the argument is not necessarily evaluated before the function call. It should be noted that this does not mean that the dependency annotations of arguments are ignored completely. If the body of a function makes use of an argument, the type system makes sure that its dependency annotation is also incorporated into the result.

When constructing a pair (rule [T-Pair]), the dependency annotations of the components are stored in the type while the pair itself is assigned the least dependency annotation. When accessing a component of a pair (rule [T-Proj]), we require that the dependency annotation of the pair matches the dependency annotation of the projected component. Again, this is no restriction due to the subtyping rule.

In [T-Inl/Inr], the argument to the injection constructor only determines the type and annotation of one component of the sum type while the other component can be chosen arbitrarily as long as the underlying type matches the annotation on the constructor. The destruction of sum types happens in a case statement that is handled by rule [T-Case]. Again, to keep the rule simple and without loss of precision due to judicious use of rule [T-Sub], we may demand that the types of both branches match, and that additionally the dependency annotations of both branches and the scrutinee are equal.

The annotation rule [T-Ann] requires that the dependency annotation of the term being annotated is at least as large as the lattice element . In the fixpoint rule, [T-Fix], not only the types but also the dependency annotations of the term itself and the bound variables must match. Note that this rule also

1 Following the literature of type and effect systems we would much like to use the term "effect" at this point, but decided to use a different term to avoid confusion with the literature on effect handlers.

Γ(x) = τ & ξ [T-Var] Σ | Γ te x : τ & ξ [T-Unit] Σ | Γ te () : unit & ⊥ Σ | Γ , x : τ1 & ξ1 te t : τ2 & ξ2 [T-Abs] Σ | Γ te λx : τ1 & ξ1.t : τ1ξ1 → τ2ξ2 & ⊥ Σ | Γ te t1 : τ1ξ1 → τ2ξ2 & ξ2 Σ | Γ te t2 : τ1 & ξ1 [T-App] Σ | Γ te t1 t2 : τ2 & ξ2 Σ | Γ te t1 : τ1 & ξ1 Σ | Γ te t2 : τ2 & ξ2 [T-Pair] Σ | Γ te (t1, t2) : τ1ξ1 × τ2ξ2 & ⊥ Σ | Γ te t : τ1ξ1 × τ2ξ2 & ξi [T-Proj] Σ | Γ te proji(t) : τi & ξi Σ | Γ te t : τ1 & ξ1 [T-Inl] Σ | Γ te inlτ-2(t) : τ1ξ1 + τ2ξ2 & ⊥ Σ | Γ te t : τ2 & ξ2 [T-Inr] Σ | Γ te inrτ-1(t) : τ1ξ1 + τ2ξ2 & ⊥ Σ | Γ te t : τ1ξ1 + τ2ξ2 & ξ Σ | Γ , y : τ2 & ξ2 te t2 : τ & ξ Σ | Γ , x : τ1 & ξ1 te t1 : τ & ξ [T-Case] Σ | Γ te **case** t **of** {inl(x ) → t1; inr(y) → t2 } : τ & ξ Σ | Γ te t : τ & ξ Σ sub ξ [T-Ann] Σ | Γ te ann(t) : τ & ξ Σ | Γ , x : τ & ξ te t : τ & ξ [T-Fix] Σ | Γ te μx : τ & ξ.t : τ & ξ Σ | Γ te t1 : τ1 & ξ Σ | Γ te t2 : τ2 & ξ [T-Seq] Σ | Γ te seq t1 t2 : τ2 & ξ Σ | Γ te t : τ & ξ Σ sub τ τ Σ sub ξ ξ [T-Sub] Σ | Γ te t : τ & ξ Σ,β : κ | Γ te t : τ & ξ β ∈ fav(Γ) ∪ fav(ξ) [T-AnnAbs] Σ | Γ te Λβ :: κ.t : ∀β :: κ.τ & ξ Σ | Γ te t : ∀β :: κ.τ & ξ Σ s ξ : κ [T-AnnApp] Σ | Γ te t ξ : [ξ / β]τ & ξ Fig. 6: Declarative annotated type system (Σ | Γ te t : τ & ξ)

v ∈ **Nf** ::= λx : τ & ξ.t | Λβ :: κ.t | () | inlτ (t) | inrτ (t) | (t1, t2) v ∈ **Nf** ::= v | ann(v )

Fig. 7: Values in the target language

admits polyvariant recursion [23], since quantification can occur anywhere in an annotated type. Since seq *t*1 *t*2 forces the evaluation of its first argument, it requires that *t*1's dependency annotation is part of the final result. This is justified, because the result depends on the termination behavior of *t*1.

The subtyping rule [T-Sub] allows us to weaken the annotations nested inside a type through the subtyping relation (see figure 5), as well as the dependency annotations itself through the subsumption relation. The rule [T-AnnAbs] introduces an annotation variable β of sort κ in the body t of the abstraction. The second premise ensures that the annotation variable does not escape its scope determined by the quantification on the type level. The annotation application rule [T-AnnApp] allows the instantiation of an annotation variable with an arbitrary well-sorted dependency term.

# **5 Metatheory**

In this section we develop a noninterference proof for our declarative type system, based on a small-step operational call-by-name semantics for the target language.

Figure 7 defines the values of the target language, i.e. those terms that cannot be further evaluated. Apart from a technicality related to annotations, they correspond exactly to the weak head normal forms of terms. The distinction for **Nf** ⊂ **Nf** is made to ensure that there is at most one annotation at top level.

The semantics itself is largely straightforward, except for the handling of annotations. These are moved just as far outwards as necessary in order to reach a normal form, thereby computing the least "permission" an evaluator must possess for computing a certain output. Figure 8 shows two rules: a lifting rule (for applications) and the rule for merging adjacent annotations (see the supplemental material for the others).

In the remainder of this section we state the standard *progress* and *subject reduction* theorems that ensure that our small-step semantics is compatible with

$$\frac{v' \in \mathbf{Mf}'}{\left(\text{ann}\_{\ell}(v')\right) t\_2 \to \text{ann}\_{\ell}(v'|t\_2)} \text{ [E-LirrtApp]}$$

$$\frac{v' \in \mathbf{Mf}'}{\text{ann}\_{\ell\_1}(\text{ann}\_{\ell\_2}(v')) \to \text{ann}\_{\ell\_1 \sqcup \ell\_2}(v')} \text{ [E-JoinANN]}$$

Fig. 8: Small-step semantics (*t* → *t* ) (excerpt)

the annotated type system. The following progress theorem demonstrates that any well-typed term is in normal form, or an evaluation step can be performed.

**Theorem 1 (Progress).** *If* ∅|∅te *t* : τ & ξ*, then either* t ∈ **Nf** *or there is a t such that t* → *t .*

The subject reduction property says that the reduction of a well-typed term results in a term of the same type.

**Theorem 2 (Subject Reduction).** *If* ∅|∅te *t* : τ& ξ *and there is a t such that t* → *t , then* ∅|∅te *t* : τ & ξ*.*

As expected, subject reduction extends naturally to a sequence of reductions by induction on the length of the reduction sequence:

**Corollary 1.** *If we have* ∅|∅te *t* : τ & ξ *and t* →∗ *v , then* ∅|∅te *v* : τ & ξ*.*

where, as usual, we write *t* →∗ *v* if there is a finite sequence of terms (ti)0in with t0 = t and tn = v ∈ **Nf** and reductions (ti → ti+1)0i<n between them. If there is no such sequence, this is denoted by t ⇑ and t is said to *diverge*.

Finally, if a term evaluates to an annotated value, this annotation is compatible with the dependency annotation that has been assigned to the term:

**Theorem 3 (Semantic Soundness).** *If we have* ∅|∅te *t* : τ & ξ *and t* →∗ ann(*v* )*, then* ∅ sub ξ*.*

**The noninterference property** An important theorem for the safety of program transformations/optimizations using the results of dependency analysis is *noninterference*. It guarantees that if there is a target term *t* depending on some variable *x* such that ∅ | *x* :τ &ξ te *t*:τ&ξ holds and the dependency annotation ξ of the variable is not encompassed by the resulting dependency annotation ξ (i.e. ∅ sub ξ ξ), then *t* will always evaluate to the same normal form, regardless the value of *x* .

Since we are in a non-strict setting, our noninterference property only applies to the topmost constructors of values. This is because the dependency annotations derived in the annotated type system only provide information about the evaluation to weak head normal form. Nested terms might possess lower as well as higher classifications. In particular, the subterms with greater dependency annotations than their enclosing constructors prevent us from making a more general statement because those can still depend on the context whereas the toplevel constructor cannot. In the noninterference theorem presented for the SLam calculus, this problem is circumvented by restricting the statement to so called *transparent* types, where the annotations of nested components are decreasing when moving further inward [9].

In the following we consider two normal forms v1, v2 ∈ **Nf** to be *similar*, denoted v1 v2, if their top level constructors (and annotations, if present) match (see the supplemental material for the unsurprising definition of ). So, v1 v2 implies that these two values are indistinguishable without further evaluation, which is the property guaranteed by the noninterference theorem.

**Theorem 4 (Noninterference).** *Let t be a target term such that* ∅ | *x* : τ & ξ te *t* : τ & ξ *and* ∅sub ξ ξ*. Let v be a value.*

*If there is a t*1 *with* ∅|∅te *t*1 : τ & ξ *such that* [*t*1 / *x* ]*t* →∗ *v , then there is a t such that for all t*2 *with* ∅|∅te *t*2 : τ & ξ *we have* [*t*2 / *x* ]*t* →∗ [*t*2 / *x* ]*t and* [*t*1 / *x* ]*t* [*t*2 / *x* ]*t .*

The noninterference proofs crucially rely on the fact that the source term is well-typed, and the additional assumption ∅ sub ξ ξ stating that the dependency annotation of the variable in the context is not encompassed by the dependency annotation of the term being evaluated.

By introducing the restriction to transparent types, we can recover the notion of noninterference used for the SLam calculus. For example, if we have a transparent type τ1ξ1 × τ2ξ2 & ξ (i.e. ∅sub ξ1 ξ and ∅sub ξ2 ξ) and ∅ sub ξ ξ holds, then we also know ∅ sub ξ ξ1 and ∅ sub ξ ξ2. Otherwise, we would get ∅ sub ξ ξ by transitivity, contradicting the assumption. This means all prerequisites of the noninterference theorem are still fulfilled.

Hence, it is possible in these cases to apply the noninterference theorem to the nested (possibly unevaluated) subterms of a constructor in weak head normal form. As in the work of [1], our noninterference theorem is restricted to deal with terms depending on exactly one variable.

# **6 The type reconstruction algorithm**

**Modularity considerations** When designing the type reconstruction algorithm we have two goals: it should be a conservative extension of the underlying type system, and types assigned by the analysis should be as general as possible. Concretely, a function's type must be general enough to be able to adapt to arguments with arbitrary annotations. These two goals give rise to the notion of *fully flexible* and *fully parametric* types defined by [12]. [16] calls these types *conservative* and *pattern* types respectively. Informally, an annotated type is a pattern type if it can be instantiated to any conservative type of the same shape and a conservative type is an analysis of an expression that is able to cope with any arguments it might depend on. These types are conservative in the sense that they make the least assumptions about their arguments and therefore are a conservative estimate compared to other typings with fewer degrees of freedom.

For a pattern type to be instantiable to any conservative type, we first need to make sure that all dependency annotations occurring in it can be instantiated to the corresponding dependency terms in a matching conservative type. This leads to the following definition of a *pattern* in the λ-calculus. It is based on the similar definition by [16] which in turn is a special case of a pattern in higher-order unification theory [4,21]. A λ-term is a *pattern* if it is of the form f β1 ··· βn where f is a free variable and β1,...,βn are distinct bound variables. A unification problem of the form ∀β1 ··· βn.f β1 ··· βn = ξ where the left-hand side is a pattern is called *pattern unification*. A pattern unification problem ∀β1 ··· βn.f β1 ··· βn = ξ has a unique most general solution, namely the substitution [f → λβ1. ··· λβn.ξ] [4].

β ∈ αi [P-Unit] αi :: καi p unit & β αi β :: καi ⇒ αi :: καi p τ1 & ξ1 βj :: κβj αi :: καi p τ2 & ξ2 γk :: κγk [P-Prod] αi :: καi p τ1ξ1 × τ2ξ2 & β αi β :: καi ⇒ , βj :: κβj , γk :: κγk ∅ p τ1 & ξ1 βj :: κβj αi :: καi , βj :: κβj p τ2 & ξ2 γk :: κγk [P-Arr] αi :: καi p ∀βj :: κβj .τ1ξ1 → τ2ξ2 & β αi β :: καi ⇒ , γk :: κγk

Fig. 9: Pattern types (Σ p τ& ξ
Σ ), where β ∈ αi, βj , γk , and [P-Sum] is like [P-Prod]

The definition of a pattern is then extended to annotated types using the rules from figure 9. Our definition is more precise than the one from previous work in that it makes explicit which variables are expected to be bound and which are free. We require that all variables with different names in the definition of these rules are distinct from each other.

An annotated type and depencency pair τ & ξ is a *pattern type* under the sort environment Σ if the judgment Σ p τ & ξ
Σ holds for some Σ . We call the variables in Σ *argument variables* and the variables in Σ *pattern variables*.

*Example 1.* A simple pattern type with the pattern variables β :: ⇒ and β :: ⇒ ⇒ is

$$
\forall \forall \beta\_1 :: \star. \widehat{\mathtt{unit}} \langle \beta\_1 \rangle \to (\forall \beta\_2 :: \star. \widehat{\mathtt{unit}} \langle \beta\_2 \rangle \to \widehat{\mathtt{unit}} \langle \beta' \rangle \beta\_1 \ \beta\_2 \rangle) \langle \beta \ \beta\_1 \rangle
$$

Note that since β1 is quantified on the function arrow chain, it is passed on to the second function arrow. However, it is not propagated into the second argument. In general, annotations on the return type may depend on the annotations of all previous arguments while annotations of the arguments may not. This prevents any dependency between the annotations of arguments and guarantees that they are as permissive as possible. This is also why pattern variables in a covariant position are passed on to the next higher level while pattern variables in arguments are quantified in the enclosing function arrow. This allows the caller of a function to instantiate the dependency annotations of the parameters to the actual arguments.

As we stated earlier, a conservative function type makes the least assumptions over its arguments. Formally, this means that arguments of conservative functions are pattern types. We will later see that a pattern type can be instantiated to any conservative type of the same shape. On the other hand, non-functional conservative types are not constrained in their annotations. These characteristics are captured by the following definition based on *conservative types* [16] and *fully flexible types* [12].

An annotated type τ is *conservative* if

β fresh [C-Unit] αi :: καi c unit : unit & β αi β :: καi ⇒ αi :: καi c τ1 : τ1 & ξ1 βj :: κβj αi :: καi c τ2 : τ2 & ξ2 γk :: κγk [C-Prod] αi :: καi c τ1 × τ2 : τ1ξ1 × τ2ξ2 & β αi β :: καi ⇒ , βj :: κβj , γk :: κγk ∅ c τ1 : τ1 & ξ1 βj :: κβj αi :: καi , βj :: κβj c τ2 : τ2 & ξ2 γk :: κγk [C-Arr] αi :: καi c τ1 → τ2 : ∀βj :: κβj .τ1ξ1 → τ2ξ2 & β αi β :: καi ⇒ , γk :: κγk

Fig. 10: Type completion (Σ c τ :τ&ξ
Σ ), all β fresh, [C-Sum] is like [C-Prod]

Moreover, an annotated type and depencency pair τ & ξ is *conservative* if τ is *conservative* and an annotated type environment Γ is *conservative* if for all x ∈ dom(Γ), Γ(*x* ) is conservative.

The following type signature for the function f is a conservative type that takes the function type from example 1 as an argument.

$$\begin{array}{c} f: \forall \beta: \star \Rightarrow \star. \forall \beta': \colon \star \Rightarrow \star \Rightarrow \star. \forall \beta\_3 :: \star. \\ \langle \forall \beta\_1 :: \star. \widehat{\mathtt{unit}} \langle \beta\_1 \rangle \rightarrow \langle \forall \beta\_2 :: \star. \widehat{\mathtt{unit}} \langle \beta\_2 \rangle \rightarrow \widehat{\mathtt{unit}} \langle \beta' \ \beta\_1 \ \beta\_2 \rangle \rangle \langle \beta \ \beta\_1 \rangle \rangle \langle \beta\_3 \rangle \\ \rightarrow \widehat{\mathtt{unit}} \langle \beta\_3 \sqcup \beta \perp \sqcup \bot \beta' \perp \ell \rangle \ \& \ \bot \end{array}$$

Note that the pattern variables of the argument have been bound in the top-level function type. This allows callers of f to instantiate these patterns.

We can extend the previous definition of pattern types to the type completion relation shown in figure 10. It relates every underlying type τ with a pattern type τ such that τ erases to τ . It is defined through judgments Σ c τ : τ&ξ
Σ with the meaning that under the sort environment Σ, τ is completed to the annotated type τ and the dependency annotation ξ containing the pattern variables Σ . The completion relation can also be interpreted as a function taking Σ and τ as arguments and returning τ, ξ and Σ .

Lastly, we revisit the examples from the previous sections and show how a pattern type can be mechanically derived from an underlying type.

In example 1 we presented a pattern type for the underlying type unit → unit → unit. Using the type completion relation, we can derive the pattern type,

$$\begin{aligned} \langle \forall \beta\_1 . \widehat{\mathtt{unit}} \langle \beta\_1 \rangle \to \langle \forall \beta\_2 . \widehat{\mathtt{unit}} \langle \beta\_2 \rangle \to \widehat{\mathtt{unit}} \langle \beta' \ \beta\_1 \ \beta\_2 \rangle \rangle \langle \beta\_1 \beta\_2 \rangle \} \&\ \ \beta\_3 \end{aligned}$$

without having to guess. This is because the components τ, ξ and Σ in a judgment Σ c τ : τ & ξ
Σ are uniquely determined by Σ and τ from looking at the syntax alone. The resulting pattern type contains three pattern variables, β :: ⇒ , β :: ⇒ ⇒ and β3 :: . If the initial sort environment is empty, these are also the only free variables of the pattern type.

Based on the type completion relation we can define least type completions. These are conservative types that are subtypes of all other conservative types of the same shape. Therefore, all annotations occurring in positive positions on the top level function arrow chain must also be least. We do not need to consider arguments here because those are by definition equal up to alpha-conversion due to being pattern types. We define the *least annotation term* of sort κ as

$$\begin{aligned} \bot\_{\star} &= \bot\\ \bot\_{\kappa\_1 \Rightarrow \kappa\_2} &= \lambda \beta : \kappa\_1 . \bot\_{\kappa\_2} . \end{aligned}$$

These least annotation terms correspond to the least elements of our bounded lattice for a given sort κ. This in turn leads us to the definition of the least completion of type τ (see figure 10) by substituting all free variables in the completion with the least annotation of the corresponding sort, i.e.

$$\bot\_{\tau} = [\overline{\bot\_{\kappa\_i} / \beta\_i}] \widehat{\tau} \text{ for } \emptyset \vdash\_c \tau : \widehat{\tau} \text{ \& } \xi \rhd \overline{\beta\_i :: \kappa\_i} \dots$$

**The algorithm** We can now move on to the type reconstruction algorithm that performs the actual analysis. At its core lies algorithm R shown in figure 11. The input of the algorithm is a triple (Γ,Σ, t ) consisting of a well-typed source term t, an annotated type environment Γ providing the types and dependency annotations of the free term variables in t and a sort environment Σ mapping each free annotation variable in scope to its sort. It returns a triple *t* : τ & ξ consisting of an elaborated term *t* in the target language (that erases to the source term *t*), an annotated type τ and an dependency annotation ξ such that Σ | Γ te *t* : τ & ξ holds. In the definition of R, to avoid clutter, we write Γ instead of Γ because we are only dealing with one kind of type environment.

The algorithm relies on the invariant that all types in the type environment and the inferred type must be conservative. In the version of [16], all inferred dependency annotations (including those nested as annotations in types) had to be canonically ordered as well. But as it turned out that this canonically ordered form was not enough for deciding semantic equality, so we lifted this requirement. We still mark those places in the algorithm where canonicalization would have occurred with ··, but the actual result of this operation does not matter as long as the dependency terms remain equivalent.

The algorithm for computing the least upper bound of types ( in figure 12) requires that both types are conservative, have the same shape and use the same names for bound variables. The latter can be ensured by α-conversion while the former two requirements are fulfilled by how this function is used in R.

The restriction to conservative types allows us to ignore functions arguments because these are always required to be pattern types, which are unique up to α-equivalence. This alleviates the need for computing a corresponding greatest lower bound of types, because the algorithm only traverses covariant positions.

# R : **AnnTyEnv** × **SortEnv** × **Tm** → **Tm** × **Ty** × **AnnTm**

```
R(Γ; Σ; x ) = x : Γ(x )
R(Γ; Σ; ()) = () : unit &  ⊥
R(Γ; Σ; ann(t)) =
  let t : τ & ξ = R(Γ; Σ; t)
  in ann(t) : τ & ξ  Σ
R(Γ; Σ; seq t1 t2) =
  let t

       1 : τ1 & ξ1 = R(Γ; Σ; t1)
      t

       2 : τ2 & ξ2 = R(Γ; Σ; t2)
  in seq t

          1 t

            2 : τ2 & ξ1  ξ2Σ
R(Γ; Σ; (t1, t2)) =
  let t

       1 : τ1 & ξ1 = R(Γ; Σ; t1)
      t

       2 : τ2 & ξ2 = R(Γ; Σ; t2)
  in (t

       1, t

          2) : τ1ξ1 × τ2ξ2 & ⊥
R(Γ; Σ; inlτ2 (t)) =
  let t : τ1 & ξ1 = R(Γ; Σ; t)
  in inlτ2 (t) : τ1ξ1 + ⊥τ2 ⊥ & ⊥
R(Γ; Σ; inrτ1 (t)) =
  let t : τ2 & ξ2 = R(Γ; Σ; t)
  in inrτ1 (t) : ⊥τ1 ⊥ + τ2ξ2 & ⊥
R(Γ; Σ; case t1 of {inl(x ) → t2;
                      inr(y) → t3 }) =
  let t

       1 : τξ + τ
                   ξ
                       & ξ1 = R(Γ; Σ; t1)
      t

       2 : τ2 & ξ2 = R(Γ, x : τ & ξ; Σ; t2)
      t

       3 : τ3 & ξ3 = R(Γ, y : τ & ξ
                                    ; Σ; t3)
  in case t

            1 of {inl(x ) → t

                             2; inr(y) → t

                                          3 }
```

```
: τ2  τ3Σ & ξ1  ξ2  ξ3Σ
R(Γ; Σ; proji(t)) =
  let t : τ1ξ1 × τ2ξ2 & ξ = R(Γ; Σ; t)
  in proji(t) : τi & ξ  ξi Σ
R(Γ; Σ; λx : τ1.t) =
  let τ1 & β  βi :: κi = C([ ]; τ1)
      Γ = Γ, x : τ1 & β
      Σ = Σ, βi :: κi
     t : τ2 & ξ2 = R(Γ
                        ; Σ
                            ; t)
  in Λβi :: κi.λx : τ1 & β.t
        : ∀βi :: κi.τ1β → τ2ξ2 & ⊥
R(Γ; Σ; t1 t2) =
  let t

      1 : τ1 & ξ1 = R(Γ; Σ; t1)
      t

      2 : τ2 & ξ2 = R(Γ; Σ; t2)
      τ
       2β → τξ  βi = I(τ1)
      θ = [β → ξ2 ] ◦ M([ ]; τ
                             2; τ2)
  in t

      1 θβi t

              2 : θτΣ & ξ1  θξΣ
R(Γ; Σ; μx : τ.t) =
  do i; τ0 & ξ0 ← 0; ⊥τ & ⊥
     repeat ti+1 : τi+1 & ξi+1
                 ← R(Γ, x : τi & ξi; Σ; t)
              i ← i + 1
     until (τi−1 ≡ τi ∧ ξi−1 ≡ ξi)
     return (μx : τi & ξi.ti) : τi & ξi
```
Fig. 11: Type reconstruction algorithm (R)

The handling of λ-abstractions uses the type completion algorithm C of figure 12, that defers its work to the type completion relation defined earlier which can be interpreted in a functional way (see figure 10). The underlying type of the function argument is completed to a pattern type. The function body is analyzed in the presence of the newly introduced pattern variables. Note that this pattern type is also conservative, thereby preserving the invariant that the context only holds conservative types. The inferred annotated type of the lambda abstraction universally quantifies over all pattern variables and the quantification is reflected on the term level through annotation abstractions Λβ :: κ.*t*.

In order to analyze function applications, we need two more auxiliary algorithms. The first one is the instantiation procedure I (see figure 12) which instantiates all top-level quantifiers with fresh annotation variables. The second is the matching algorithm M (see figure 12) which instantiates a pattern type

 : **Ty** × **Ty** → **Ty** unit unit = unit (τ1ξ1 × τ2ξ2) (τ 1ξ 1 × τ 2ξ 2)=(τ1 τ 1)ξ1 ξ 1 × (τ2 τ 2)ξ2 ξ 2 (τ1β → τ2ξ2) (τ1β → τ 2ξ 2) = τ1β → (τ2 τ 2)ξ2 ξ 2 (∀β :: κ.τ) (∀β :: κ.τ ) = ∀β :: κ.τ τ

C : **SortEnv** → **Ty** × **AnnTm** × **SortEnv** C(Σ; τ ) = τ & ξ βi :: κi **where** Σ c τ : τ & ξ βi :: κi

I : **Ty** → **Ty** × **SortEnv** I(∀β :: κ.τ) = **let** τ Σ = I(τ) **in** [β → β ](τ ) β :: κ, Σ **where** β be fresh I(τ) = τ [ ]

M : **SortEnv** × **Ty** × **Ty** → **AnnSubst** M(Σ; unit; unit) = [ ] M(Σ; τ 1β βi × τ 2β βi; τ1ξ1 × τ2ξ2) = [β → λβi :: Σ(βi).ξ1, β → λβi :: Σ(βi).ξ2 ] ◦ M(Σ; τ 1; τ1) ◦ M(Σ; τ 2; τ2) M(Σ; τ1β → τ 2β βi; τ1β → τ2ξ) = [β → λβi :: Σ(βi).ξ ] ◦ M(Σ; τ 2; τ2) M(Σ; ∀β :: κ.τ ; ∀β :: κ.τ) = M(Σ,β :: κ; τ ; τ)

Fig. 12: Least upper bound of types ( ), completion (C), instantiation (I), and matching (M). Rules for · + · in and M are like those for ·×·.

with a conservative type of the same shape. It returns a substitution obtained by performing pattern unification on corresponding annotations.

**Soundness and Completeness** An annotated type environment Γ is wellformed under an environment Σ, if Γ is conservative and for all bindings *x* : τ&ξ in Γ we have Σ wft τ and Σ s ξ : .

In order to demonstrate the correctness of the reconstruction algorithm presented in this section we have to show that for every well-typed underlying term, it produces an analysis (i.e. annotated types and dependency annotations) that can be derived in the annotated type system (see figure 6). That is to say, algorithm R is sound w.r.t. the annotated type system.

**Theorem 5.** *Let t be a source term,* Σ *a sort environment and* Γ *an annotated type environment well-formed under* Σ *such that* R(Γ; Σ; *t*) = *t* : τ& ξ *for some t ,* τ *and* ξ*.*

*Then,* Σ | Γ te *t* : τ & ξ*,* Σ wft τ*,* Σ s ξ : *and* τ *is conservative.*

The next step is to show that our analysis succeeds in deriving an annotated type and dependency annotation for any well-typed source term: it is *complete*. The crucial part here is the termination of the fixpoint iteration. In order to show the convergence of the fixpoint iteration, we start by defining an equivalence relation on annotated type and depencency pairs.

Our type reconstruction algorithm handles polymorphic recursion through Kleene-Mycroft-iteration. Such an algorithm is based on fixpoint iteration and needs a way to decide whether two dependency terms are equal according to the denotational semantics of λ.

A straightforward way to decide semantic equivalence is to enumerate all possible environments and compare the denotations of the two terms in all of these (possibly after some semantics preserving normalization). This only works if the dependency lattice L is finite.

For some analyses, e.g., the set of all program locations in a slicing analysis, L = V is finite but large, and deciding equality in this fashion becomes impractical. To alleviate this problem, our prototype implementation applies a partial canonicalization procedure which, while not complete, can serve as an approximation of equality: if two canonicalized dependency terms become syntactically equal, then we can be assured that they are semantically equal, but if they are not we can still apply the above procedure to the canonicalized dependency terms. We omit formal details from the paper.

We can now state our completeness results for the type reconstruction algorithm. Here, we write Γ t *t* : τ to say that term *t* has type τ under the environment Γ in the underlying type system.

**Theorem 6 (Completeness).** *Given a source term* t*, a sort environment* Σ*, an annotated type environment* Γ *well-formed under* Σ*, and an underlying type* τ *such that* Γ t *t* : τ *, then there are t ,* τ *and* ξ *such that* R(Γ; Σ; *t*) = *t* : τ&ξ *and* τ = τ *, t* = *t .*

As a corollary of the foregoing theorems, our analysis is a conservative extension of the underlying type system.

**Corollary 2 (Conservative Extension).** *Let* t *be a source term,* τ *be a type and* Γ *a type environment such that* Γ t *t* : τ *. Then there are* Σ*,* Γ*, t ,* τ*,* ξ *such that* Σ | Γ te *t* : τ & ξ *with t* = *t ,* τ = τ *and* Γ = Γ*.*

# **7 Implementation and Examples**

Beyond the definition of the annotated system and the development of the associated algorithm and meta-theory we also have a REPL prototype implementation of our analysis in Haskell. Compared to the annotated type system in the paper, the prototype provides support for booleans and integers, including literals and conditionals **if** *c* **then** *t*1 **else** *t*2 for which the type rules can be straightforwardly derived. Concrete lattice implementations are provided only for bindingtime analysis and security analysis, but the reconstruction algorithm abstracts away from the choice for a particular lattice, so it is easy to add new instances. The implementation is available at http://www.staff.science.uu.nl/∼hage0101/ prototype-hrp.zip. Below we walk through a few examples, taking advantage of the slightly extended source language that our implementation supports. More (detailed) examples are discussed in [26].

**Construction and Elimination** Whenever something is constructed, be it a product, a sum or a lambda abstraction, the outermost dependency annotation is ⊥. This is because the analysis aims to produce the best possible and thereby least annotations for a given source program.

Consider the case of binding-time analysis, and suppose we have a variable of function type *f* :∀β.intβ → intβ&**D**. We can see that it preserves the annotations of its arguments, i.e. if we apply f to a static value, the return annotation is also instantiated to be static. The function itself, however, is dynamic. And therefore, the whole result of the function application must also be dynamic, because we cannot know which particular function has been assigned to *f* .

As elimination always introduces a dependency in the program, and this can uncover subtleties arising when functions only differ in their termination behavior. For example, compare λ*p* : int×int.*p* with λ*p* : int×int.(proj1(*p*), proj2(*p*)). In a call-by-value language, these two functions would be (extensionally) equivalent. However, with non-strict evaluation, *p* might be a non-terminating computation. In that case, applying the former function would diverge, while the latter function at least produces the pair constructor. This is also reflected in the annotated types that are inferred. For the former, we get

$$\forall \beta\_0, \beta\_1, \beta\_2 :: \star. (\text{int}\langle \beta\_0 \rangle \times \text{int}\langle \beta\_1 \rangle) \langle \beta\_2 \rangle \rightarrow (\text{int}\langle \beta\_0 \rangle \times \text{int}\langle \beta\_1 \rangle) \langle \beta\_2 \rangle \& \mathbf{S}, \text{and}$$

$$\forall \beta\_0, \beta\_1, \beta\_2 :: \star \text{.} \langle \text{int} \langle \beta\_0 \rangle \times \text{int} \langle \beta\_1 \rangle \rangle \langle \beta\_2 \rangle \to \langle \text{int} \langle \beta\_0 \sqcup \beta\_2 \rangle \times \text{int} \langle \beta\_1 \sqcup \beta\_2 \rangle \rangle \langle \mathbf{S} \rangle \text{ \& } \mathbf{S}$$

for the latter. In particular, the annotation of the product in the second type signature is **S**. Therefore, it can not depend on the input of the function.

**Polymorphic Recursion** One class of functions where the analysis benefits from polymorphic recursion are those that permute their arguments on recursive calls. Our example is a slightly modified version of an example from [5]:

$$\text{\(\mu f:\text{bool}\to\text{bool}\to\text{bool}.\lambda x:\text{bool}.\lambda y:\text{bool}.\text{ if }x\text{ then }true\text{ else }f\text{ }y\text{ }x$$

In an analysis with monomorphic recursion, the analysis assigns the same annotation to both parameters, large enough to accommodate for both arguments. This is due to the permutation of the arguments in the else branch. An analysis with polymorphic recursion is allowed to use a different instantiation for f in that case. Our algorithm hence infers the following most general type.

$$\forall \beta\_1 :: \star \widehat{\text{bool}} \langle \beta\_1 \rangle \to (\forall \beta\_2 :: \star \widehat{\text{bool}} \langle \beta\_2 \rangle \to \widehat{\text{bool}} \langle \beta\_1 \sqcup \beta\_2 \rangle) \langle \perp \rangle \&\perp$$

We see that the result of the function indeed depends on the annotations of both arguments, as both end up in the condition of the if-expression at some point. Yet, both arguments are completely unrestricted, and unrelated in their annotations. In contrast, a type system with monomorphic recursion would only admit a weaker type, possibly similar to

$$
\forall \beta\_1 :: \star. \mathsf{bool} \langle \beta\_1 \rangle \to (\mathsf{bool} \langle \beta\_1 \rangle \to \mathsf{bool} \langle \beta\_1 \rangle) \langle \bot \rangle \&\perp.
$$

A real world example of this kind is Euclid's algorithm for computing the greatest common divisor(see [26]).

**Higher-Ranked Polyvariance** This section discusses several examples for the dependency analysis instance of binding time analysis, comparing our outcomes with a let-polyvariant analysis[29].

A simple example to start with is a function that applies a function to both components of a pair2

*both* : (int → int) → int × int → int × int *both* = λ*f* : int → int.λ*p* : int × int.(*f* (proj1(*p*)), *f* (proj2(*p*)))

Suppose in the context of binding-time analysis that *both* is used to apply a statically known function to a pair whose first component is always computable at compile time, but whose second component is dynamic. For simplicity's sake, the function is the identity on integers.

*id* : int → int *id* = λ*x* : int.*x*

A non-higher-ranked analysis would assign types to *both* and *id*. The annotation on the function argument to *both* must be large enough to accommodate both components of the pair as input. When we consider the call *both id p* for some pair *p*:int**S**×int**D**&**S**. Then, the whole call has the type int**D**×int**D**.

Our higher-ranked analysis infers the following conservative types for *id* and *both*.

$$\begin{array}{lcl} \left(id : \forall \beta :: \star \text{.int}\langle\beta\rangle \rightarrow \text{int}\langle\beta\rangle\ \&\bot\\ \left(id = A\beta :: \star \lambda x : \text{int}\ \beta\right.\right.\\ \left(both : \forall \beta\_{1} :: \star \lambda \forall\_{2} :: \star \Rightarrow \star. (\forall\beta :: \star. \text{int}\langle\beta\rangle \rightarrow \text{int}\langle\beta\_{2}\ \beta\rangle)\langle\beta\_{1}\rangle\\ \quad \rightarrow (\forall\beta\_{3}, \beta\_{4}, \beta\_{5} :: \star. (\text{int}\langle\beta\_{3}\rangle \times \text{int}\langle\beta\_{4}\rangle)\langle\beta\_{5}\rangle\\ \quad \rightarrow (\text{int}\langle\beta\_{2}\ (\beta\_{3} \sqcup \beta\_{5}) \sqcup \beta\_{1}\rangle \times \text{int}\langle\beta\_{2}\ (\beta\_{4} \sqcup \beta\_{5}) \sqcup \beta\_{1}\rangle)\langle\mathbf{S}\rangle\ \&\mathbf{S}\\ \left(both = A\beta\_{1} :: \star. A\beta\_{2} :: \star \Rightarrow \star. \text{f}\ \beta :: (\forall\beta :: \star. \text{int}\langle\beta\rangle \rightarrow \text{int}\langle\beta\_{2}\ \beta\rangle)\right).\\ \left(A\beta\_{3} :: \star. A\beta\_{4} :: \star. A\beta\_{5} :: \star. \lambda p :: \text{int}\langle\beta\_{3}\rangle \times \text{int}\langle\beta\_{4}\rangle)\\ \quad \left(f \mid \beta\_{3} \sqcup \beta\_{5}\right)\left(\text{proj}\_{1}(p)\right), f \mid \beta\_{4} \sqcup \beta\_{5}\rangle\left(\text{proj}\_{2}(p)\right))\end{array}\right)$$

In case of *both*, the function parameter f can be instantiated separately for each component because our analysis assigns it a type that universally quantifies over

2 NB. both is a simplified instance of a traversal ∀f .Applicative f ⇒ (Int → f Int) → (Int,Int) → f (Int,Int), in order to fit the restrictions of the source language [6,15].

the annotation of its argument. It is evident from the type signature that the components of the resulting pair only depend on the corresponding components of the input pair, and the function and the input pair itself. They do not depend on the respective other component of the input.

If we again consider the call *both id p*, we obtain β2 = λβ :: .β, β1 = β3 = β5 = **S** and β4 = **D** through pattern unification. Normalization of the resulting dependency terms results in the expected return type int**S** × int**D**.

The generality provided by the higher-ranked analysis extends to an arbitrarily deep nesting of function arrows. The following example demonstrates this for two levels of arrows. Functions with more than two levels of arrows can arise directly in actual programs, but even more so in desugared code, e.g., when type classes in Haskell are implemented via explicit dictionary passing. Due to limitations of our source language, the examples are syntactically heavily restricted.

Consider the following function that takes a function argument which again requires a function.

 $foo : ((\text{int} \rightarrow \text{int}) \rightarrow \text{int}) \rightarrow \text{int} \times \text{int}$   $foo = \lambda f : (\text{int} \rightarrow \text{int}) \rightarrow \text{int}.(f \ (\lambda x : \text{int}.x), f \ (\lambda x : \text{int}.0))$

The higher-ranked analysis infers the following type and target term (where we omitted the type in the argument of the lambda term because it essentially repeats what is already visible in the top level type signature).

$$\begin{array}{lcll} foo : \forall \beta\_{4} :: \star \forall \beta\_{3} :: \star \Rightarrow (\star \Rightarrow \star) \Rightarrow \star. \\ (\forall \beta\_{2} :: \star. \forall \beta\_{1} :: \star \Rightarrow. (\forall \beta\_{0} :: \star. \text{int} \langle \beta\_{0} \rangle \rightarrow \text{int} \langle \beta\_{1} \mid \beta\_{0})) \langle \beta\_{2} \rangle \\ \rightarrow \text{int} \langle \beta\_{3} \; \beta\_{2} \; \beta\_{1} \rangle \langle \beta\_{4} \rangle \\ \rightarrow \text{int} \langle \beta\_{3} \; \mathbf{S} \; \big( \lambda \beta\_{5} :: \star. \beta\_{5} \big) \sqcup \beta\_{4} \rangle \times \text{int} \langle \beta\_{3} \; \mathbf{S} \; \big( \lambda \beta\_{6} :: \star. \mathbf{S} \big) \sqcup \beta\_{4} \rangle \langle \big{) \mathbf{S} \rangle \& \ \mathbf{S} \\ \rightarrow \text{int} \langle \beta\_{4} :: \star.  Therefore, the analysis of f depends on the analysis of the function passed to it. This gives rise to the *higher-order effect operator* β3 [12]. Thus, f can be applied to any function with a conservative type of the right shape. As our algorithm always infers conservative types, the type of f is as general as possible. This is reflected in the body of the lambda where in both cases f is instantiated with the dependency annotation corresponding to the function passed to it. The result of this instantiation can be observed in the returned product type where β3 is applied to the effect operators λβ0 :: .β0 and λβ0 :: .**S** corresponding to the respective functions used as arguments to f.

 \Lambda \alpha\_{1} :: \star \Rightarrow \star. \lambda f : \begin{array}{c} \neg . f \end{array} \begin{array}{c} \mathsf{ann\_{D}(0)) \end{array} \end{array}$$

For *bar* we obtain *foo bar* : int**D** × int**S** & **S**. In this case, β3 = λβ2 :: .λβ1 :: ⇒ .β1 **D** β2, because *bar* applies its argument to a value with dynamic binding time. This causes the first component of the returned pair to be deemed dynamic as well. On the other hand, in the second component *bar* is applied to a constant function. Thus, regardless of the argument's dynamic binding time, the resulting binding time is static. In a rank-1 system we would get int**D** × int**D** instead of int**D** × int**S**.

# **8 Related Work**

The basis for most type systems of functional programming languages is the Hindley-Milner type system [22]. Our algorithm *R* strongly resembles the wellknown type inference algorithm for the Hindley-Milner type system, *Algorithm W* [3], a distinct advantage of our approach. The idea to define an annotated type system as a means to design static analyses for higher-order languages is attributed to [19]. The major technical difference compared to a let-polyvariant analysis is that our annotations form a simply typed lambda-calculus.

Full reconstruction for a higher-ranked polyvariant annotated type system was first considered by [12] in the context of a control-flow analysis. However, we found that the (constraint-based) algorithm as presented in [12] generates constraints free of cycles. Therefore, it cannot faithfully reflect the constraints necessary for the fixpoint combinator. The algorithm incorrectly concludes for the following example that only the first and third 'False' term flow into the condition *x* , but not the second one.

#### (*fix* (λ*f* . λ*x* . λ*y*. λ*z* . **if** *x* **then** *True* **else** *fzxy*)) *False False False*

We reproduced this mistake with their implementation and verified that the mistake was not a simple bug in that implementation.

Close to our formulation is the (unpublished) work of [16] which deals with exception analysis, which uses a simply typed lambda-calculus with sets to represent annotations. We have chosen a more modular approach in which we offload much of the complexity of dealing with lattice values to the lattice. In [16] terms from the simply typed lambda-calculus with sets are canonicalized and then checked for alpha equivalence during Kleene-Mycroft iteration. We found however that two terms can have different canonical forms even though they are actually semantically equivalent. This causes Koot's reconstruction algorithm to diverge on a particular class of programs, because the inferred annotations continue to grow. The simplest such program we found is the following.

μ*f* : (unit → unit) → unit → unit.λ*g* : unit → unit.λ*x* : unit.*g* (*f gx* )

Our solution is to apply canonicalization to simplify terms as much as possible, and then compare the outcomes for all possible inputs.

The Dependency Core Calculus was introduced by [1] as a unifying framework for dependency analyses. Instances include binding-time analysis (see, e.g., [29]), exception analysis [17,16], secure information flow analysis [9] and static slicing [27]. They devised the *Dependency Core Calculus* (DCC) to which each instance of a dependency analysis can be mapped. This allowed them to compare different dependency analyses, uncover problems with existing instance analyses and to simplify proofs of noninterference [8,20]. The instance analyses in [1] were defined as a monovariant type and effect system with subtyping, for a monomorphic call-by-name language. An implicit, let-polymorphic implementation of DCC, FlowCaml, was developed by [25]. It is not higher-ranked.

The difference between DCC and our analysis is to a large extent a different focus: the DCC is a calculus defined in a way that any calculus that elaborates to DCC has the noninterference property and any other properties proven for the calculus. On the other hand, our analysis is meant to be implemented in a compiler (with the added precision), and that implementation (and its associated meta-theory) can then be reused inside the compiler for a variety of analyses. Comparable to DCC, we have proven a noninterference property for our generic higher-rank polyvariant dependency analysis, so that all its instances inherit it.

The Haskell community supports an implementation of DCC in which the (security) annotations are lifted to the Haskell type level [2]. Since the GHC compiler supports higher-rank types, the code written with this library can in fact model security flows with higher-rank. Because of the general undecidability of full reconstruction for higher-rank types [14], the programmer must however provide explicit type information. In [18], the authors introduce dependent flow types, that allows them to express a large variety of security policies. An essential difference with our work is that our approach is fully automated.

Early on in our research, we observed that the approach of [11] may lead to similar precision gains as higher-ranked annotations do. Since they deal with a different analysis, a direct comparison is impossible to make at this time.

# **9 Conclusion and Future Work**

We have defined a higher-rank annotation polymorphic type system for a generic dependency analysis, established its soundness and provided a sound and complete reconstruction algorithm. Examples show that we can achieve higher precision than plain let-polyvariance. The analysis we have defined is for a call-byname language. We expect the results to hold as well for a lazy language, but chose call-by-name for reduced bookkeeping in the proofs. We also believe the analysis can be adapted relatively easily to one for a call-by-value language, by letting the annotation on the argument flow into the effect of the call. However, we would need to re-examine the metatheory.

In future work we want to consider whether we can further refine the canonicalization of λ terms so that syntactic equality up to alpha-equivalence can completely replace our current approach.

**Acknowledgments** We acknowledge the contributions of Ruud Koot in unpublished work that made this work possible.

# **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs**

John Toman1, Ren Siqi1, Kohei Suenaga1 , Atsushi Igarashi1 , and Naoki Kobayashi2

1 Kyoto University, Kyoto, Japan<EMAIL_ADDRESS>2 The University of Tokyo, Tokyo, Japan<EMAIL_ADDRESS>
**Abstract.** We present ConSORT, a type system for safety verification in the presence of mutability and aliasing. Mutability requires strong updates to model changing invariants during program execution, but aliasing between pointers makes it difficult to determine which invariants must be updated in response to mutation. Our type system addresses this difficulty with a novel combination of refinement types and fractional ownership types. Fractional ownership types provide flow-sensitive and precise aliasing information for reference variables. ConSORT interprets this ownership information to soundly handle strong updates of potentially aliased references. We have proved ConSORT sound and implemented a prototype, fully automated inference tool. We evaluated our tool and found it verifies non-trivial programs including data structure implementations.

**Keywords:** refinement types, mutable references, aliasing, strong updates, fractional ownerships, program verification, type systems

# **1 Introduction**

Driven by the increasing power of automated theorem provers and recent highprofile software failures, fully automated program verification has seen a surge of interest in recent years [5, 10, 15, 29, 38, 66]. In particular, refinement types [9, 21, 24, 65], which refine base types with logical predicates, have been shown to be a practical approach for program verification that are amenable to (sometimes full) automation [47, 61, 62, 63]. Despite promising advances [26, 32, 46], the sound and precise application of refinement types (and program verification in general) in settings with mutability and aliasing (e.g., Java, Ruby, etc.) remains difficult.

One of the major challenges is how to precisely and soundly support strong updates for the invariants on memory cells. In a setting with mutability, a single invariant may not necessarily hold throughout the lifetime of a memory cell; while the program mutates the memory the invariant may change or evolve. To model these changes, a program verifier must support different, incompatible invariants which hold at different points during program execution. Further, precise program verification requires supporting different invariants on distinct pieces of memory.

```
1 mk(n) { mkref n }
3 let p = mk(3) in
4 let q = mk(5) in
5 p := *p + 1;
6 q := *q + 1;
7 assert(*p = 4);
```
**Fig. 1.** Example demonstrating the difficulty of effecting strong updates in the presence of aliasing. The function mk is bound in the program from lines 3 to 7; its body is given within the braces.

```
1 loop(a, b) {
2 let aold = *a in
3 b := *b + 1;
4 a := *a + 1;
5 assert(*a = aold + 1);
6 if -
        then
7 loop(b, mkref -
                     )
8 else
9 loop(b,a)
10 }
11 loop(mkref -
              , mkref -
                        )
```
**Fig. 2.** Example with non-trivial aliasing behavior.

One solution is to use refinement types on the static program names (i.e., variables) which point to a memory location. This approach can model evolving invariants while tracking distinct invariants for each memory cell. For example, consider the (contrived) example in Figure 1. This program is written in an MLlike language with mutable references; references are updated with := and allocated with **mkref**. Variable p can initially be given the type {ν : **int** | ν = 3} **ref**, indicating it is a reference to the integer 3. Similarly, q can be given the type {ν : **int** | ν = 5} **ref**. We can model the mutation of p's memory on line 5 by strongly updating p's type to {ν : **int** | ν = 4} **ref**.

Unfortunately, the precise application of this technique is confounded by the existence of unrestricted aliasing. In general, updating just the type of the mutated reference is insufficient: due to aliasing, other variables may point to the mutated memory and their refinements must be updated as well. However, in the presence of conditional, may aliasing, it is impossible to strongly update the refinements on all possible aliases; given the static uncertainty about whether a variable points to the mutated memory, that variable's refinement may only be weakly updated. For example, suppose we used a simple alias analysis that imprecisely (but soundly) concluded all references allocated at the same program point might alias. Variables p and q share the allocation site on line 1, so on line 5 we would have to weakly update q's type to {ν : **int** | ν = 4 ∨ ν = 5}, indicating it may hold either 4 or 5. Under this same imprecise aliasing assumption, we would also have to weakly update p's type on line 6, preventing the verification of the example program.

Given the precision loss associated with weak updates, it is critical that verification techniques built upon refinement types use precise aliasing information and avoid spuriously applied weak updates. Although it is relatively simple to conclude that p and q do not alias in Figure 1, consider the example in Figure 2. (In this example, represents non-deterministic values.) Verifying this program requires proving a and b never alias at the writes on lines 3 and 4. In fact, a and b may point to the same memory location, but only in different invocations of loop; this pattern may confound even sophisticated symbolic alias analyses. Additionally, a and b share an allocation site on line 7, so an approach based on the simple alias analysis described above will also fail on this example. This mustnot alias proof obligation can be discharged with existing techniques [53, 54], but requires an expensive, on-demand, interprocedural, flow-sensitive alias analysis.

This paper presents ConSORT (CONtext Sensitive Ownership Refinement Types), a type system for the automated verification of program safety in imperative languages with mutability and aliasing. ConSORT is built upon the novel combination of refinement types and fractional ownership types [55, 56]. Fractional ownership types extend pointer types with a rational number in the range [0, 1] called an ownership. These ownerships encapsulate the permission of the reference; only references with ownership 1 may be used for mutation. Fractional ownership types also obey the following key invariant: any references with a mutable alias must have ownership 0. Thus, any reference with non-zero ownership cannot be an alias of a reference with ownership 1. In other words, ownerships encode precise aliasing information in the form of must-not aliasing relationships.

To understand the benefit of this approach, let us return to Figure 1. As mk returns a freshly allocated reference with no aliases, its type indicates it returns a reference with ownership 1. Thus, our type system can initially give p and q types {ν : **int** | ν = 3} **ref** 1 and {ν : **int** | ν = 5} **ref** 1 respectively. The ownership 1 on the reference type constructor **ref** indicates both pointers hold "exclusive" ownership of the pointed to reference cell; from the invariant of fractional ownership types p and q must not alias. The types of both references can be strongly updated without requiring spurious weak updates. As a result, at the assertion statement on line 7, p has type {ν : **int** | ν = 4} **ref** 1 expressing the required invariant.

Our type system can also verify the example in Figure 2 without expensive side analyses. As a and b are both mutated, they must both have ownership 1; i.e., they cannot alias. This pre-condition is satisfied by all invocations of loop; on line 7, b has ownership 1 (from the argument type), and the newly allocated reference must also have ownership 1. Similarly, both arguments on line 9 have ownership 1 (from the assumed ownership on the argument types).

Ownerships behave linearly; they cannot be duplicated, only split when aliases are created. This linear behavior preserves the critical ownership invariant. For example, if we replace line 9 in Figure 2 with loop(b,b), the program becomes ill-typed; there is no way to divide b's ownership of 1 to into two ownerships of 1.

Ownerships also obviate updating refinement information of aliases at mutation. ConSORT ensures that only the trivial refinement is used in reference types with ownership 0, i.e., mutably-aliased references. When memory is mutated through a reference with ownership 1, ConSORT simply updates the refinement of the mutated reference variable. From the soundness of ownership types, all aliases have ownership 0 and must therefore only contain the refinement. Thus, the types of all aliases already soundly describe all possible contents.3

ConSORT is also context-sensitive, and can use different summaries of function behavior at different points in the program. For example, consider the variant

3 This assumption holds only if updates do not change simple types, a condition our type-system enforces.

```
1 get(p) { *p }
3 let p = mkref 3 in
4 let q = mkref 5 in
5 p := get(p) + 1;
6 q := get(q) + 1;
7 assert(*p = 4);
8 assert(*q = 6);
```
**Fig. 3.** Example of context-sensitivity

of Figure 1 shown in Figure 3. The function get returns the contents of its argument, and is called on lines 5 and 6. To precisely verify this program, on line 5 get must be typed as a function that takes a reference to 3 and returns 3. Similarly, on line 6 get must be typed as a function that takes a reference to 5 and returns 5. Our type system can give get a function type that distinguishes between these two calling contexts and selects the appropriate summary of get's behavior.

We have formalized ConSORT as a type system for a small imperative calculus and proved the system is sound: i.e., a well-typed program never encounters assertion failures during execution. We have implemented a prototype type inference tool targeting this impera-

tive language and found it can automatically verify several non-trivial programs, including sorted lists and an array list data structure.

The rest of this paper is organized as follows. Section 2 defines the imperative language targeted by ConSORT and its semantics. Section 3 defines our type system and states our soundness theorem. Section 4 sketches our implementation's inference algorithm and its current limitations. Section 5 describes an evaluation of our prototype, Section 6 outlines related work, and Section 7 concludes.

# **2 Target Language**

This section describes a simple imperative language with mutable references and first-order, recursive functions.

#### **2.1 Syntax**

We assume a set of variables, ranged over by x, y, z, . . . , a set of function names, ranged over by f, and a set of labels, ranged over by 1, 2,... . The grammar of the language is as follows.

$$\begin{array}{l} d ::= f \mapsto (x\_1, \ldots, x\_n)e \\ e ::= x \mid \textbf{let}\, x = y \,\textbf{in}\, e \mid \textbf{let}\, x = n \,\textbf{in}\, e \mid \textbf{ifz}\, x \,\textbf{then}\, e\_1 \,\textbf{else}\, e\_2 \\ \mid & \textbf{let}\, x = \textbf{mkre}\, y \,\textbf{in}\, e \mid \textbf{let}\, x = \*y \,\textbf{in}\, e \mid \textbf{let}\, x = f^\ell(y\_1, \ldots, y\_n) \,\textbf{in}\, e \\ \mid & x ::= y \,\textbf{;} e \mid \textbf{allis}\,(x = y) \,\textbf{;} e \mid \textbf{allis}\,(x = \*y) \,\textbf{;} e \mid \textbf{assert}(\varphi) \,; e \mid e\_1 \,\textbf{;} e\_2 \\ \mid & P ::= \langle \{d\_1, \ldots, d\_n\}, e \rangle \end{array}$$

ϕ stands for a formula in propositional first-order logic over variables, integers and contexts; we discuss these formulas later in Section 3.1.

Variables are introduced by function parameters or let bindings. Like ML, the variable bindings introduced by let expressions and parameters are immutable. Mutable variable declarations such as int x = 1; in C are achieved in our language with:

```
let y = 1 in(let x = mkref y in ...) .
```
As a convenience, we assume all variable names introduced with let bindings and function parameters are distinct.

Unlike ML (and like C or Java) we do not allow general expressions on the right hand side of let bindings. The simplest right hand forms are a variable y or an integer literal n. **mkref** y creates a reference cell with value y, and ∗y accesses the contents of reference y. For simplicity, we do not include an explicit null value; an extension to support null is discussed in Section 4. Function calls must occur on the right hand side of a variable binding and take the form f -(x1,..., xn), where x1,..., xn are distinct variables and is a (unique) label. These labels are used to make our type system context-sensitive as discussed in Section 3.3.

The single base case for expressions is a single variable. If the variable expression is executed in a tail position of a function, then the value of that variable is the return value of the function, otherwise the value is ignored.

The only intraprocedural control-flow operations in our language are if statements. **ifz** checks whether the condition variable x equals zero and chooses the corresponding branch. Loops can be implemented with recursive functions and we do not include them explicitly in our formalism.

Our grammar requires that side-effecting, result-free statements, **assert**(ϕ) **alias**(x = y), **alias**(x = ∗y) and assignment x := y are followed by a continuation expression. We impose this requirement for technical reasons to ease our formal presentation; this requirement does not reduce expressiveness as dummy continuations can be inserted as needed. The **assert**(ϕ); e form executes e if the predicate ϕ holds in the current state and aborts the program otherwise. **alias**(x = y); e and **alias**(x = ∗y); e assert a must-aliasing relationship between x and y (resp. x and ∗y) and then execute e. **alias** statements are effectively annotations that our type system exploits to gain added precision. x : = y ; e updates the contents of the memory cell pointed to by x with the value of y. In addition to the above continuations, our language supports general sequencing with e1 ; e2.

A program is a pair D, e, where D = {d1, ... , dn} is a set of first-order, mutually recursive function definitions, and e is the program entry point. A function definition d maps the function name to a tuple of argument names x1, ... , xn that are bound within the function body e.

Paper Syntax. In the remainder of the paper, we will write programs that are technically illegal according to our grammar, but can be easily "de-sugared" into an equivalent, valid program. For example, we will write

**let** x = **mkref** 4 **in assert**(\*x = 4)

as syntactic sugar for:

**let** f=4 **in let** x = **mkref** f **in let** tmp = \*x **in assert**(tmp = 4); **let** dummy = 0 **in** dummy

#### **2.2 Operational Semantics**

We now introduce the operational semantics for our language. We assume a finite domain of heap addresses **Addr**: we denote an arbitrary address with a.

**Fig. 4.** Transition Rules (1).

A runtime state is represented by a configuration - H , R, F , e , which consists of a heap, register file, stack, and currently reducing expression respectively. The register file maps variables to runtime values v, which are either integers n or addresses a. The heap maps a finite subset of addresses to runtime values. The runtime stack represents pending function calls as a sequence of return contexts, which we describe below. While the final configuration component is an expression, the rewriting rules are defined in terms of E[e], which is an evaluation context E and redex e, as is standard. The grammar for evaluation contexts is defined by: E ::= E ; e | [].

Our operational semantics is given in Figures 4 and 5. We write dom(H ) to indicate the domain of a function and H {a → v} where a ∈ dom(H ) to denote a map which takes all values in dom(H) to their values in H and which additionally takes a to v. We will write H {a ← v} where a ∈ dom(H ) to denote a map equivalent to H except that a takes value v. We use similar notation for dom(R) and R{x → v}. We also write ∅ for the empty register file and heap. The step relation −→D is parameterized by a set of function definitions D; a program D, e is executed by stepping the initial configuration ∅, ∅, ·, e according to −→D . The semantics is mostly standard; we highlight some important points below.

Return contexts F take the form E[**let** y = [] **in** e]. A return context represents a pending function call with label , and indicates that y should be bound to the return value of the callee during the execution of e within the larger execution context E. The call stack F is a sequence of these contexts, with the first such return context representing the most recent function call. The stack grows at function calls as described by rule R-Call. For a call E[**let** x = f -(y1,..., yn)**in** e] where f is defined as (x1, ... , xn)e , the return context E[**let** y = []**in** e] is

f → (x1, .. , xn )e ∈ D - H , R, F , E[**let** x = f -(y1,..., yn ) **in** e- ] −→D - H , R, E[**let** x = [] **in** e- ] : F , [y1/x1] ··· [yn /xn ]e (R-Call) R(x) = a a ∈ dom(H ) - H , R, F , E[x : = y ; e] −→D - H {a ← R(y)}, R, F , E[e] (R-Assign) R(x) = R(y) - H , R, F , E[**alias**(x = y) ; e] −→D - H , R, F , E[e] (R-Alias) R(y) = a H (a) = R(x) - H , R, F , E[**alias**(x = ∗y) ; e] −→D - H , R, F , E[e] (R-AliasPtr) R(x) = R(y) - H , R, F , E[**alias**(x = y) ; e] −→D **AliasFail** (R-AliasFail) R(x) = H (R(y)) - H , R, F , E[**alias**(x = ∗y) ; e] −→D **AliasFail** (R-AliasPtrFail) |= [R] ϕ - H , R, F , E[**assert**(ϕ) ; e] −→D - H , R, F , E[e] (R-Assert) |= [R] ϕ - H , R, F , E[**assert**(ϕ) ; e] −→D **AssertFail** (R-AssertFail)

**Fig. 5.** Transition Rules (2).

prepended onto the stack of the input configuration. The substitution of formal arguments for parameters in e , denoted by [y1/x1] ··· [yn/xn]e , becomes the currently reducing expression in the output configuration. Function returns are handled by R-Var. Our semantics return values by name; when the currently executing function fully reduces to a single variable x, x is substituted into the return context on the top of the stack, denoted by E[**let** y = []**in** e][x].

In the rules R-Assert we write |= [R] ϕ to mean that the formula yielded by substituting the concrete values in R for the variables in ϕ is valid within some chosen logic (see Section 3.1); in R-AssertFail we write |= [R] ϕ when the formula is not valid. The substitution operation [R] ϕ is defined inductively as [∅] ϕ = ϕ, [R{x → n}] ϕ = [R] [n/x ]ϕ, [R{x → a}] ϕ = [R] ϕ. In the case of an assertion failure, the semantics steps to a distinguished configuration **AssertFail**. The goal of our type system is to show that no execution of a well-typed program may reach this configuration. The **alias** form checks whether the two references actually alias; i.e., if the must-alias assertion provided by the programmer is correct. If not, our semantics steps to the distinguished **AliasFail** configuration. Our type system does not guarantee that **AliasFail** is unreachable; aliasing assertions are effectively trusted annotations that are assumed to hold.

In order to avoid duplicate variable names in our register file due to recursive functions, we refresh the bound variable x in a let expression to x . Take expression **let** x = y **in** e as an example; we substitute a fresh variable x for x in e, then bind x to the value of variable y. We assume this refreshing of variables preserves our assumption that all variable bindings introduced with let and function parameters are unique, i.e. x does not overlap with variable names that occur in the program.

Types τ ::= {ν : **int** | ϕ} | τ **ref** r Ownership r ∈ [0, 1] Refinements ϕ ::= ϕ1 ∨ ϕ2 | ¬ϕ | | φ(v-1, .. , vn ) | v-1 = v-2 | CP Ref. Values v- ::= x | n | ν Function Types σ ::= ∀λ.x1 : τ1,..., xn : τn → x1 : τ - 1,..., xn : τ - n | τ Context Variables λ ∈ **CVar** Concrete Context ::= : | Pred. Context C ::= : C | λ | Context Query CP ::= C Typing Context L ::= λ |

**Fig. 6.** Syntax of types, refinements, and contexts.

# **3 Typing**

We now introduce a fractional ownership refinement type system that guarantees well-typed programs do not encounter assertion failures.

#### **3.1 Types and Contexts**

The syntax of types is given in Figure 6. Our type system has two type constructors: references and integers. τ **ref** r is the type of a (non-null) reference to a value of type τ . r is an ownership which is a rational number in the range [0, 1]. An ownership of 0 indicates a reference that cannot be written, and for which there may exist a mutable alias. By contrast, 1 indicates a pointer with exclusive ownership that can be read and written. Reference types with ownership values between these two extremes indicate a pointer that is readable but not writable, and for which no mutable aliases exist. ConSORT ensures that these invariants hold while aliases are created and destroyed during execution.

Integers are refined with a predicate ϕ. The language of predicates is built using the standard logical connectives of first-order logic, with (in)equality between variables and integers, and atomic predicate symbols φ as the basic atoms. We include a special "value" variable ν representing the value being refined by the predicate. For simplicity, we omit the connectives ϕ1 ∧ ϕ2 and ϕ1 =⇒ ϕ2; they can be written as derived forms using the given connectives. We do not fix a particular theory from which φ are drawn, provided a sound (but not necessarily complete) decision procedure exists. CP are context predicates, which are used for context sensitivity as explained below.

Example 1. {ν : **int** | ν > 0} is the type of strictly positive integers. The type of immutable references to integers exactly equal to 3 can be expressed by {ν : **int** | ν = 3} **ref** 0.5.

As is standard, we denote a type environment with Γ, which is a finite map from variable names to type τ . We write Γ[x : τ ] to denote a type environment Γ such that Γ(x ) = τ where x ∈ dom(Γ), Γ, x : τ to indicate the extension of Γ with the type binding x : τ , and Γ[x ← τ ] to indicate the type environment Γ with the binding of x updated to τ . We write the empty environment as •. The treatment of type environments as mappings instead of sequences in a dependent type system is somewhat non-standard. The standard formulation based on ordered sequences of bindings and its corresponding well-formedness condition did not easily admit variables with mutually dependent refinements as introduced by our function types (see below). We therefore use an unordered environment and relax well-formedness to ignore variable binding order.

Function Types, Contexts, and Context Polymorphism. Our type system achieves context sensitivity by allowing function types to depend on where a function is called, i.e., the execution context of the function invocation. Our system represents a concrete execution contexts with strings of call site labels (or just "call strings"), defined by ::= | : . As is standard (e.g., [49, 50]), the string : abstracts an execution context where the most recent, active function call occurred at call site which itself was executed in a context abstracted by ; is the context under which program execution begins. Context variables, drawn from a finite domain **CVar** and ranged over by λ1, λ2,..., represent arbitrary, unknown contexts.

A function type takes the form ∀λ.x1 : τ1,..., xn : τn→x1 : τ 1,..., xn : τ n | τ . The arguments of a function are an n-ary tuple of types τi. To model side-effects on arguments, the function type includes the same number of output types τ i . In addition, function types have a direct return type τ . The argument and output types are given names: refinements within the function type may refer to these names. Function types in our language are context polymorphic, expressed by universal quantification "∀λ." over a context variable. Intuitively, this context variable represents the many different execution contexts under which a function may be called.

Argument and return types may depend on this context variable by including context query predicates in their refinements. A context query predicate CP usually takes the form λ, and is true iff is a prefix of the concrete context represented by λ. Intuitively, a refinement λ =⇒ ϕ states that ϕ holds in any concrete execution context with prefix , and provides no information in any other context. In full generality, a context query predicate may be of the form 1 2 or 1 ...n : λ; these forms may be immediately simplified to , ⊥ or λ.

Example 2. The type {ν : **int** | (1 λ =⇒ ν = 3) ∧ (2 λ =⇒ ν = 5)} represents an integer that is 3 if the most recent active function call site is 1, 5 if the most recent call site is 2, and is otherwise unconstrained. This type may be used for the argument of f in, e.g., f-1 (3) + f-2 (5).

As types in our type system may contain context variables, our typing judgment (introduced below) includes a typing context L, which is either a single context variable λ or a concrete context . This typing context represents the assumptions about the execution context of the term being typed. If the typing context is a context variable λ, then no assumptions are made about the execution context of the term, although types may depend upon λ with context query predicates. Accordingly, function bodies are typed under the context variable universally quantified over in the corresponding function type; i.e., no assumptions are made about the exact execution context of the function body. As in parametric polymorphism, consistent substitution of a concrete context for a context variable λ in a typing derivation yields a valid type derivation under concrete context .

Remark 1. The context-sensitivity scheme described here corresponds to the standard CFA approach [50] without a priori call-string limiting. We chose this scheme because it can be easily encoded with equality over integer variables (see Section 4), but in principle another context-sensitivity strategy could be used instead. The important feature of our type system is the inclusion of predicates over contexts, not the specific choice for these predicates.

Function type environments are denoted with Θ and are finite maps from function names (f ) to function types (σ).

Well Formedness. We impose two well-formedness conditions on types: ownership well-formedness and refinement well-formedness. The ownership condition is purely syntactic: τ is ownership well-formed if τ = τ **ref** 0 implies τ = n for some n. i is the "maximal" type of a chain of i references, and is defined inductively as 0 = {ν : **int** | } , i = i−1 **ref** 0.

The ownership well-formedness condition ensures that aliases introduced via heap writes do not violate the invariant of ownership types and that refinements are consistent with updates performed through mutable aliases. Recall our ownership type invariant ensures all aliases of a mutable reference have 0 ownership. Any mutations through that mutable alias will therefore be consistent with the "no information" refinement required by this well-formedness condition.

Refinement well-formedness, denoted L | Γ WF ϕ, ensures that free program variables in refinement ϕ are bound in a type environment Γ and have integer type. It also requires that for a typing context L = λ, only context query predicates over λ are used (no such predicates may be used if L = ). Notice this condition forbids refinements that refer to references. Although ownership information can signal when refinements on a mutably-aliased reference must be discarded, our current formulation provides no such information for refinements that mention mutably-aliased references. We therefore conservatively reject such refinements at the cost of some expressiveness in our type system.

We write L | Γ WF τ to indicate a well-formed type where all refinements are well-formed with respect to L and Γ. We write L WF Γ for a type environment where all types are well-formed. A function environment is well-formed (written WF Θ) if, for every σ in Θ, the argument, result, and output types are wellformed with respect to each other and the context variable quantified over in σ. As the formal definition of refinement well-formedness is fairly standard, we omit it for space reasons (the full definition may be found in the full version [60]).

#### **3.2 Intraprocedural Type System**

We now introduce the type system for the intraprocedural fragment of our language. Accordingly, this section focuses on the interplay of mutability and

$$\begin{array}{|c|c|c|c|c|}
\hline
\Theta & \mathcal{L} & \Gamma[x : \tau\_1 + \tau\_2] \vdash x : \tau\_1 \Rightarrow \Gamma[x \stackrel{\sim}{\longrightarrow} \tau\_2] \\
\hline
\end{array}$$

Θ |L| Γ[y ← τ1 ∧y y =τ1 x], x : (τ2 ∧x x =τ2 y) e : τ ⇒ Γ x ∈ dom(Γ- ) Θ |L| Γ[y : τ1 + τ2] **let** x = y **in** e : τ ⇒ Γ-(T-Let)

$$\frac{\Theta \mid \mathcal{L} \mid \varGamma, x:\{\nu:\mathsf{int} \mid \nu = n\} \vdash e:\tau \Rightarrow \varGamma' \qquad x \notin \hom(\varGamma')}{\Theta \mid \mathcal{L} \mid \varGamma \vdash \mathsf{let}\, x = n \,\mathsf{in}\, e:\tau \Rightarrow \varGamma'} \tag{\mathsf{T}\text{-}\text{L\text{str}\,\text{Intr}}}$$

$$\begin{array}{c} \Theta \mid \mathcal{L} \mid \Gamma[\boldsymbol{x} \Longleftarrow \{\boldsymbol{\nu} : \mathsf{int} \mid \boldsymbol{\varphi} \land \boldsymbol{\nu} = 0\}] \vdash e\_1 : \boldsymbol{\tau} \Rightarrow \boldsymbol{\Gamma}' \\ \Theta \mid \mathcal{L} \mid \Gamma[\boldsymbol{x} \Longleftarrow \{\boldsymbol{\nu} : \mathsf{int} \mid \boldsymbol{\varphi} \land \boldsymbol{\nu} \neq 0\}] \vdash e\_2 : \boldsymbol{\tau} \Rightarrow \boldsymbol{\Gamma}' \\ \hline \Theta \mid \mathcal{L} \mid \Gamma[\boldsymbol{x} : \{\boldsymbol{\nu} : \mathsf{int} \mid \boldsymbol{\varphi}\}] \vdash \mathsf{ifz} \, x \, \mathsf{then} \, e\_1 \, \mathsf{else} \, e\_2 : \boldsymbol{\tau} \Rightarrow \boldsymbol{\Gamma}' \end{array} \tag{\mathsf{T-Ir}}$$

Θ |L| Γ[y ← τ1], x : (τ2 ∧x x =τ2 y) **ref** 1 e : τ ⇒ Γ- x ∈ dom(Γ- ) Θ |L| Γ[y : τ1 + τ2] **let** x = **mkref** y **in** e : τ ⇒ Γ- (T-MkRef) Θ |L| Γ e1 : τ- ⇒ Γ- Θ |L| Γ- e2 : τ-- ⇒ Γ-- Θ |L| Γ e1 ; e2 : τ-- ⇒ Γ-- (T-Seq)

$$\begin{array}{c} \tau' = \begin{cases} \tau\_{1} \wedge\_{y} \, y = \tau\_{1} \, & x \, \, r > 0\\ \tau\_{1} & \, r = 0\\ \Theta \mid \mathcal{L} \mid \Gamma[y \xleftarrow{\tau'} \, \mathtt{ref}^{r}], x : \tau\_{2} \vdash e : \tau \Rightarrow \Gamma'\\ x \notin \mathit{dom}(\Gamma')\\ \end{array} & \begin{array}{c} \Gamma \mid \Rightarrow \varphi \quad \epsilon \mid \Gamma \vdash\_{WF} \varphi\\ \Theta \mid \mathcal{L} \mid \Gamma \vdash\_{e} : \tau \Rightarrow \Gamma'\\ \end{array} \\ \begin{array}{c} \Theta \mid \mathcal{L} \mid \Gamma \vdash \mathtt{assert}(\varphi); e : \tau \Rightarrow \Gamma'\\ \end{array} & \begin{array}{c} \tau \mid \mathcal{L} \mid \Gamma \vdash\_{\mathtt{NF}} \varphi\\ \end{array} \\ \end{array}$$

**Fig. 7.** Expression typing rules.

refinement types. The typing rules are given in Figures 7 and 8. A typing judgment takes the form Θ |L| Γ e : τ ⇒ Γ , which indicates that e is well-typed under a function type environment Θ, typing context L, and type environment Γ, and evaluates to a value of type τ and modifies the input environment according to Γ . Any valid typing derivation must have L WF Γ, L WF Γ , and L | Γ WF τ , i.e., the input and output type environments and result type must be well-formed.

The typing rules in Figure 7 handle the relatively standard features in our language. The rule T-Seq for sequential composition is fairly straightforward except that the output type environment for e1 is the input type environment for e2. T-LetInt is also straightforward; since x is bound to a constant, it is given type {ν : **int** | ν = n} to indicate x is exactly n. The output type environment Γ cannot mention x (expressed with x ∈ dom(Γ )) to prevent x from escaping its scope. This requirement can be met by applying the subtyping rule (see below) to weaken refinements to no longer mention x . As in other refinement type systems [47], this requirement is critical for ensuring soundness.

Rule T-Let is crucial to understanding our ownership type system. The body of the let expression e is typechecked under a type environment where the type of y in Γ is linearly split into two types: τ1 for y and τ2 for the newly created binding x . This splitting is expressed using the + operator. If y is a reference type, the split operation distributes some portion of y's ownership information to its new alias x . The split operation also distributes refinement information between the two types. For example, type {ν : **int** | ν > 0} **ref** 1 can be split into (1) {ν : **int** | ν > 0} **ref** r and {ν : **int** | ν > 0} **ref** (1−r) (for r ∈ (0, 1)),

i.e., two immutable references with non-trivial refinement information, or (2) {ν : **int** | ν > 0} **ref** 1 and {ν : **int** | } **ref** 0, where one of the aliases is mutable and the other provides no refinement information. How a type is split depends on the usage of x and y in e. Formally, we define the type addition operator as the least commutative partial operation that satisfies the following rules:

$$\begin{aligned} \{\nu : \mathbf{int} \mid \varphi\_1\} + \{\nu : \mathbf{int} \mid \varphi\_2\} &= \{\nu : \mathbf{int} \mid \varphi\_1 \land \varphi\_2\} & \text{(TAD-INT)}\\ \tau\_1 \, \mathbf{ref}^{r\_1} + \tau\_2 \, \mathbf{ref}^{r\_2} &= (\tau\_1 + \tau\_2) \, \mathbf{ref}^{r\_1 + r\_2} & \text{(TADn-REF)} \end{aligned}$$

Viewed another way, type addition describes how to combine two types for the same value such that the combination soundly incorporates all information from the two original types. Critically, the type addition operation cannot create or destroy ownership and refinement information, only combine or divide it between types. Although not explicit in the rules, by ownership well-formedness, if the entirety of a reference's ownership is transferred to another type during a split, all refinements in the remaining type must be .

The additional bits ∧yy =τ1 x and ∧xx =τ2 y express equality between x and y as refinements. We use the strengthening operation τ ∧x ϕ and typed equality proposition x =τ y, defined respectively as:

$$\begin{aligned} \{\nu: \mathsf{int} \mid \varphi\} \wedge\_y \varphi' &= \{\nu: \mathsf{int} \mid \varphi \wedge \left[\nu/y\right] \varphi'\} & & (x =\_{\{\nu: \mathsf{int} \mid \varphi\}} y) = (x = y) \\ \tau \,\mathsf{ref}^r \wedge\_y \varphi' &= \tau \,\mathsf{ref}^r & & (x =\_{\tau \,\mathsf{ref}^r} y) = \top \end{aligned}$$

We do not track equality between references or between the contents of aliased reference cells as doing so would violate our refinement well-formedness condition. These operations are also used in other rules that can introduce equality.

Rule T-MkRef is very similar to T-Let, except that x is given a reference type of ownership 1 pointing to τ2, which is obtained by splitting the type of y. In T-Deref, the content type of y is split and distributed to x . The strengthening is conditionally applied depending on the ownership of the dereferenced pointer, that is, if r = 0, τ has to be a maximal type i.

Our type system also tracks path information; in the T-If rule, we update the refinement on the condition variable within the respective branches to indicate whether the variable must be zero. By requiring both branches to produce the same output type environment, we guarantee that these conflicting refinements are rectified within the type derivations of the two branches.

The type rule for assert statements has the precondition Γ |= ϕ which is defined to be |= -Γ =⇒ ϕ, i.e., the logical formula -Γ =⇒ ϕ is valid in the chosen theory. -Γ lifts the refinements on the integer valued variables into a proposition in the logic used for verification. This denotation operation is defined as:

$$\begin{array}{ll} \left[\begin{smallmatrix} \bullet\\ \Gamma, x:\tau \end{smallmatrix} \right] = \top & \left[\begin{smallmatrix} \left\{\nu:\mathsf{int}\right\}\left\vert\varphi\right\} \right]\_y = \left[y/\,\nu\right]\varphi\\ \left[\begin{smallmatrix} \tau\\ \end{smallmatrix}\right] = \left[\begin{smallmatrix} \tau\\ \end{smallmatrix}\right] \land \left[\begin{smallmatrix} \tau\\ \end{smallmatrix}\right]\_x & \left[\begin{smallmatrix} \tau'\textbf{ }\textbf{ref}^r\end{smallmatrix}\right]\_y = \top \end{array} \end{array}$$

If the formula -Γ =⇒ ϕ is valid, then in any context and under any valuation of program variables that satisfy the refinements in -Γ, the predicate ϕ must be true and the assertion must not fail. This intuition forms the foundation of our soundness claim (Section 3.4).

696 J. Toman et al.

$$\frac{\Theta \mid \mathcal{L} \mid I \left[ x \xleftarrow{} \tau\_1 \right] \left[ y \iff \left( \tau\_2 \land\_y y =\_{\tau\_2} x \right) \mathsf{ref}^1 \right] \vdash e : \tau \Rightarrow I'}{\Theta \mid \mathcal{L} \mid I \left[ x \mathrel{\mathop{:}} \tau\_1 + \tau\_2 \right] \left[ y \mathrel{\mathop{:}} \tau' \text{ \textbf{ref}^1} \right] \vdash y : = x ; e : \tau \Rightarrow I'} \tag{\text{\textbf{T-AssCNN}}}$$

$$\begin{array}{c} \left(\tau\_{1}\operatorname{ref}^{r\_{1}} + \tau\_{2}\operatorname{ref}^{r\_{2}}\right) \approx \left(\tau\_{1}^{\prime}\operatorname{ref}^{r\_{1}^{\prime}} + \tau\_{2}^{\prime}\operatorname{ref}^{r\_{2}^{\prime}}\right) \\ \Theta \mid \mathcal{L} \mid \Gamma[x \longleftarrow \tau\_{1}^{\prime}\operatorname{ref}^{r\_{1}^{\prime}}][y \longleftarrow \tau\_{2}^{\prime}\operatorname{ref}^{r\_{2}^{\prime}}] \vdash e : \tau \Rightarrow \Gamma' \\ \hline \Theta \mid \mathcal{L} \mid \Gamma[x : \tau\_{1}\operatorname{ref}^{r\_{1}^{\prime}}][y : \tau\_{2}\operatorname{ref}^{r\_{2}^{\prime}}] \vdash \operatorname{allias}(x = y) : e : \tau \Rightarrow \Gamma' \end{array} \tag{\mathcal{T}\text{-}\operatorname{A}\mathbf{1}\text{.} \text{a}\text{s}})$$

$$\begin{array}{c} (\tau\_1 \operatorname{ ref}^{r\_1} + \tau\_2 \operatorname{ ref}^{r\_2}) \approx (\tau\_1' \operatorname{ ref}^{r\_1'} + \tau\_2' \operatorname{ ref}^{r\_2'})\\ \Theta \mid \mathcal{L} \mid \Gamma[x \longleftarrow \tau\_1' \operatorname{ ref}^{r\_1}][y \longleftarrow (\tau\_2' \operatorname{ ref}^{r\_2'}) \operatorname{ ref}^{r}] \vdash e : \tau \Rightarrow \Gamma'\\ \hline \Theta \mid \mathcal{L} \mid \Gamma[x : \tau\_1 \operatorname{ ref}^{r\_1}][y : (\tau\_2 \operatorname{ ref}^{r\_2}) \operatorname{ ref}^{r}] \vdash \operatorname{ alias} (x = \*y) : e : \tau \Rightarrow \Gamma' \end{array} \tag{\text{T-Aıl.s}\operatorname{Pr}}$$

$$\frac{\Gamma \le \Gamma' \qquad \Theta \mid \mathcal{L} \mid \Gamma' \vdash e : \tau \Rightarrow \Gamma' \qquad \Gamma''', \tau \le \Gamma'''', \tau'}{\Theta \mid \mathcal{L} \mid \Gamma \vdash e : \tau' \Rightarrow \Gamma'''} \tag{\text{T-Sva}}$$

τ1 ≈ τ2 iff • τ1 ≤ τ2 and • τ2 ≤ τ1.

**Fig. 8.** Pointer manipulation and subtyping

Γ |= ϕ1 =⇒ ϕ2 Γ {ν : **int** | ϕ1}≤{ν : **int** | ϕ2} (S-Int) r1 ≥ r2 Γ τ1 ≤ τ2 Γ τ1 **ref** r1 ≤ τ2 **ref** r2 (S-Ref) ∀ x ∈ dom(Γ- ).Γ Γ(x) ≤ Γ- (x) Γ ≤ Γ- (S-TyEnv) Γ, x : τ ≤ Γ- , x : τ x ∈ dom(Γ) Γ, τ ≤ Γ, τ-(S-Res)

**Fig. 9.** Subtyping rules.

Destructive Updates, Aliasing, and Subtyping. We now discuss the handling of assignment, aliasing annotations, and subtyping as described in Figure 8. Although apparently unrelated, all three concern updating the refinements of (potentially) aliased reference cells.

Like the binding forms discussed above, T-Assign splits the assigned value's type into two types via the type addition operator, and distributes these types between the right hand side of the assignment and the mutated reference contents. Refinement information in the fresh contents may be inconsistent with any previous refinement information; only the shapes must be the same. In a system with unrestricted aliasing, this typing rule would be unsound as it would admit writes that are inconsistent with refinements on aliases of the left hand side. However, the assignment rule requires that the updated reference has an ownership of 1. By the ownership type invariant, all aliases with the updated reference have 0 ownership, and by ownership well-formedness may only contain the refinement.

Example 3. We can type the program as follows:

```
let x = mkref 5 in // x : {ν : int | ν = 5} ref 1
let y=x in // x : 1, y : {ν : int | ν = 5} ref 1
 y := 4; assert(*y = 4) // x : 1, y : {ν : int | ν = 4} ref 1
```
In this and later examples, we include type annotations within comments. We stress that these annotations are for expository purposes only; our tool can infer these types automatically with no manual annotations.

As described thus far, the type system is quite strict: if ownership has been completely transferred from one reference to another, the refinement information found in the original reference is effectively useless. Additionally, once a mutable pointer has been split through an assignment or let expression, there is no way to recover mutability. The typing rule for must alias assertions, T-Alias and T-AliasPtr, overcomes this restriction by exploiting the must-aliasing information to "shuffle" or redistribute ownerships and refinements between two aliased pointers. The typing rule assigns two fresh types τ 1 **ref** r- 1 and τ 2 **ref** r- 2 to the two operand pointers. The choice of τ 1, r 1, τ 2, and r 2 is left open provided that the sum of the new types, (τ 1 **ref** r- 1 )+(τ 2 **ref** r- 2 ) is equivalent (denoted ≈) to the sum of the original types. Formally, ≈ is defined as in Figure 8; it implies that any refinements in the two types must be logically equivalent and that ownerships must also be equal. This redistribution is sound precisely because the two references are assumed to alias; the total ownership for the single memory cell pointed to by both references cannot be increased by this shuffling. Further, any refinements that hold for the contents of one reference must necessarily hold for contents of the other and vice versa.

```
Example 4 (Shuffling ownerships and refinements). Let ϕ=n be ν = n.
```
**let** x = **mkref** 5 **in** // x : {ν : **int** | ϕ=5} **ref** 1 **let** y=x **in** // x : 1, y : {ν : **int** | ϕ=5} **ref** 1 y := 4; **alias**(x = y) // x : {ν : **int** | ϕ=4} **ref** 0.5, y : {ν : **int** | ϕ=4} **ref** 0.5

The final type assignment for x and y is justified by

$$\begin{split} & \left\{ \top\_{1} + \left\{ \nu : \mathsf{int} \mid \varphi\_{=4} \right\} \mathsf{ref}^{1} = \left\{ \nu : \mathsf{int} \mid \top \wedge \varphi\_{=4} \right\} \mathsf{ref}^{1} \approx \\ & \left\{ \nu : \mathsf{int} \mid \varphi\_{=4} \wedge \varphi\_{=4} \right\} \mathsf{ref}^{1} = \left\{ \nu : \mathsf{int} \mid \varphi\_{=4} \right\} \mathsf{ref}^{0.5} + \left\{ \nu : \mathsf{int} \mid \varphi\_{=4} \right\} \mathsf{ref}^{0.5} . \end{split}$$

The aliasing rules give fine-grained control over ownership information. This flexibility allows mutation through two or more aliased references within the same scope. Provided sufficient aliasing annotations, the type system may shuffle ownerships between one or more live references, enabling and disabling mutability as required. Although the reliance on these annotations appears to decrease the practicality of our type system, we expect these aliasing annotations can be inserted by a conservative must-aliasing analysis. Further, empirical experience from our prior work [56] indicates that only a small number of annotations are required for larger programs.

Example 5 (Shuffling Mutability). Let ϕ=n again be ν = n. The following program uses two live, aliased references to mutate the same memory location:

```
let x = mkref 0 in
let y=x in // x : {ν : int | ϕ=0} ref 1, y : 1
 x := 1; alias(x = y); // x : 1, y : {ν : int | ϕ=1} ref 1
 y := 2; alias(x = y); // x : {ν : int | ϕ=2} ref 0.5, y : {ν : int | ϕ=2} ref 0.5
 assert(*x = 2)
```

$$\begin{array}{c} \Theta(f) = \forall \lambda. \ \langle x\_{1} : \tau\_{1}, \dots, x\_{n} : \tau\_{n} \rangle \to \langle x\_{1} : \tau'\_{1}, \dots, x\_{n} : \tau'\_{n} \mid \tau \rangle \\ \sigma\_{\alpha} = \left[ \ell : \mathcal{L} / \lambda \right] & \sigma\_{x} = \left[ y\_{1} / x\_{1} \right] \cdots \left[ y\_{n} / x\_{n} \right] \\ \Theta \mid \mathcal{L} \mid \Gamma [y\_{i} \xleftarrow \sigma\_{\alpha} \, \sigma\_{x} \, \tau'\_{i}], x : \sigma\_{\alpha} \, \sigma\_{x} \vdash e : \tau' \Rightarrow \Gamma' \qquad x \notin dom(\Gamma') \\ \hline \Theta \mid \mathcal{L} \mid \Gamma \left[ y\_{i} : \sigma\_{\alpha} \, \sigma\_{x} \, \tau\_{i} \right] \vdash \mathsf{let} \, x = f^{\ell} (y\_{1}, \dots, y\_{n}) \, \mathsf{in} \, e : \tau' \Rightarrow \Gamma' \\ \end{array} \tag{\mathsf{T-Call.}}$$

$$\begin{array}{c} \Theta(f) = \forall \lambda \, \langle x\_{1} : \tau\_{1}, \dots, x\_{n} : \tau\_{n} \rangle \to \langle x\_{1} : \tau'\_{1}, \dots, x\_{n} : \tau'\_{n} \mid \tau \rangle \\ \hline \Theta \mid \lambda \mid x\_{1} : \tau\_{1}, \dots, x\_{n} : \tau\_{n} \vdash e : \tau \Rightarrow x\_{1} : \tau'\_{1}, \dots, x\_{n} : \tau'\_{n} \end{array} \mid \tau \rangle$$

$$\begin{array}{c} \Theta \vdash f \mapsto (x\_{1}, \dots, x\_{n}) \, e \end{array} \tag{\mathsf{T-CunDEup}}$$

$$\begin{array}{c} \forall f \mapsto (x\_1, \ldots, x\_n) \, e \in D. \Theta \vdash f \mapsto (x\_1, \ldots, x\_n) \, e \\ \quad \text{dom}(D) = \text{dom}(\Theta) \\ \hline \end{array} \qquad \begin{array}{c} \quad \begin{array}{c} \quad \Theta \vdash D \\ \quad \quad \quad \vdash\_{WF} \Theta \\ \quad \quad \quad \vdash\_{\langle D,e \rangle} \\ \quad \quad \quad \vdash\_{\langle D,e \rangle} \\ \quad \quad \quad \quad \text{(T-Proof)} \end{array}$$

**Fig. 10.** Program typing rules

After the first aliasing statement the type system shuffles the (exclusive) mutability between x and y to enable the write to y. After the second aliasing statement the ownership in y is split with x ; note that transferring all ownership from y to x would also yield a valid typing.

Finally, we describe the subtyping rule. The rules for subtyping types and environments are shown in Figure 9. For integer types, the rules require the refinement of a supertype is a logical consequence of the subtype's refinement conjoined with the lifting of Γ. The subtype rule for references is covariant in the type of reference contents. It is widely known that in a language with unrestricted aliasing and mutable references such a rule is unsound: after a write into the coerced pointer, reads from an alias may yield a value disallowed by the alias' type [43]. However, as in the assign case, ownership types prevent unsoundness; a write to the coerced pointer requires the pointer to have ownership 1, which guarantees any aliased pointers have the maximal type and provide no information about their contents beyond simple types.

#### **3.3 Interprocedural Fragment and Context-Sensitivity**

We now turn to a discussion of the interprocedural fragment of our language, and how our type system propagates context information. The remaining typing rules for our language are shown in Figure 10. These rules concern the typing of function calls, function bodies, and entire programs.

We first explain the T-Call rule. The rule uses two substitution maps. σx translates between the parameter names used in the function type and actual argument names at the call-site. σα instantiates all occurrences of λ in the callee type with : L, where is the label of the call-site and L the typing context of the call. The types of the arguments yi's are required to match the parameter types (post substitution). The body of the let binding is then checked with the argument types updated to reflect the changes in the function call (again, post substitution). This update is well-defined because we require all function arguments be distinct as described in Section 2.1. Intuitively, the substitution σα represents incrementally refining the behavior of the callee function with partial context information. If L is itself a context variable λ , this substitution effectively transforms any context prefix queries over λ in the argument/return/output types into a queries over : λ . In other words, while the exact concrete execution context of the callee is unknown, the context must at least begin with which can potentially rule out certain behaviors.

Rule T-FunDef type checks a function definition f → (x1, .. , xn)e against the function type given in Θ. As a convenience we assume that the parameter names in the function type match the formal parameters in the function definition. The rule checks that under an initial environment given by the argument types the function body produces a value of the return type and transforms the arguments according to the output types. As mentioned above, functions may be executed under many different contexts, so type checking the function body is performed under the context variable λ that occurs in the function type.

Finally, the rule for typing programs (T-Prog) checks that all function definitions are well typed under a well-formed function type environment, and that the entry point e is well typed in an empty type environment and the typing context , i.e., the initial context.

Example 6 (1-CFA). Recall the program in Figure 3 in Section 1; assume the function calls are labeled as follows:

p := get-1(p) + 1; // ... q := get-2(q) + 1;

Taking τp to be the type shown in Example 2:

$$\{\nu : \mathsf{int} \mid (\ell\_1 \preceq \lambda \implies \nu = 3) \land (\ell\_2 \preceq \lambda \implies \nu = 5)\}$$

we can give get the type ∀λ. z : τp **ref** 1 → z : τp **ref** 1 | τp .

Example 7 (2-CFA). To see how context information propagates across multiple calls, consider the following change to the code considered in Example 6:

```
get_real(z) { *z }
get(z) { get_real-
                   3 (z) }
```
The type of get remains as in Example 6, and taking τ to be

$$\{\nu : \mathsf{int} \mid (\ell\_3 \ell\_1 \preceq \lambda' \implies \nu = 3) \land (\ell\_3 \ell\_2 \preceq \lambda' \implies \nu = 5)\}$$

the type of get\_real is: ∀λ . z : τ **ref** 1 → z : τ **ref** 1 | τ .

We focus on the typing of the call to get\_real in get; it is typed in context λ and a type environment where p is given type τp from Example 6.

Applying the substitution [3 : λ/λ ] to the argument type of get\_real yields:

$$\{\nu : \mathsf{int} \mid (\ell\_3 \ell\_1 \preceq \ell\_3 : \lambda \implies \nu = 3) \land (\ell\_3 \ell\_2 \preceq \ell\_3 : \lambda \implies \nu = 5)\} \,\mathsf{ref}^1 \approx$$

$$\{\nu : \mathsf{int} \mid (\ell\_1 \preceq \lambda \implies \nu = 3) \land (\ell\_2 \preceq \lambda \implies \nu = 5)\} \,\mathsf{ref}^1$$

which is exactly the type of p. A similar derivation applies to the return type of get\_real and thus get.

# **3.4 Soundness**

We have proven that any program that type checks according to the rules above will never experience an assertion failure. We formalize this claim with the following soundness theorem.

**Theorem 1 (Soundness).** If D, e, then ∅, ∅, ·, e −→∗ D **AssertFail**.

Further, any well-typed program either diverges, halts in the configuration **AliasFail**, or halts in a configuration H , R, ·, x for some H , R and x , i.e., evaluation does not get stuck.

Proof (Sketch). By standard progress and preservation lemmas; the full proof has been omitted for space reasons and can be found in the full version [60].

# **4 Inference and Extensions**

We now briefly describe the inference algorithm implemented in our tool Con-SORT. We sketch some implemented extensions needed to type more interesting programs and close with a discussion of current limitations of our prototype.

# **4.1 Inference**

Our tool first runs a standard, simple type inference algorithm to generate type templates for every function parameter type, return type, and for every live variable at each program point. For a variable x of simple type τS ::= **int** | τS **ref** at program point p, ConSORT generates a type template τSx,0,p as follows:

$$\left[\left[\mathbf{int}\right]\_{x,n,p} = \{\nu:\mathbf{int} \mid \varphi\_{x,n,p}(\nu; \mathbf{FV}\_p)\} \quad \left[\tau\_S \operatorname{ref}\right]\_{x,n,p} = \left[\tau\_S\right]\_{x,n+1,p} \operatorname{ref}^{r\_{x,n,p}}$$

ϕx,n,p(ν; **FV**p) denotes a fresh relation symbol applied to ν and the free variables of simple type **int** at program point p (denoted **FV**p). rx,n,p is a fresh ownership variable. For each function f , there are two synthetic program points, f b and f e for the beginning and end of the function respectively. At both points, ConSORT generates type template for each argument, where **FV**f b and **FV**f e are the names of integer typed parameters. At f e, ConSORT also generates a type template for the return value. We write Γp to indicate the type environment at point p, where every variable is mapped to its corresponding type template. -Γp is thus equivalent to x∈**FV**p ϕx,0,p(x ; **FV**p).

When generating these type templates, our implementation also generates ownership well-formedness constraints. Specifically, for a type template of the form {ν : **int** | ϕx,n+1,p(ν; **FV**p)} **ref** rx,n,p ConSORT emits the constraint: rx,n,p = 0 =⇒ ϕx,n+1,p(ν; **FV**p) and for a type template (τ **ref** rx,n+1,p ) **ref** rx,n,p Con-SORT emits the constraint rx,n,p =0 =⇒ rx,n+1,p = 0.