Typed Regions^{⋆}

Stefan Monnier and Zhong Shao

Department of Computer Science Yale University New Haven, CT 06520-8285

                {monnier,shao}@cs.yale.edu

Abstract. Standard type systems are not sufficiently expressive when applied to low-level memory-management code. Such code often uses some form of strong update (i.e. assignments that change the type of the affected location) and needs to reason about the relative position of objects in memory. We present a novel type system which, like alias types [20], provides a form of strong update, but with the advantage that it does not require the aliasing pattern to be statically described. It also provides operations over sequential memory locations and allows covariant reference casts. We then show how this new type system can be used to implement a type-safe stop&copy garbage collector that can properly collect cyclic datastructures. More specifically, we show how to write a two-generations collector for a language with mutable ref cells.

1 Introduction

As the technology of certifying compilation and proof carrying code [13, 1, 6] has progressed, the need to ensure the safety of the runtime system has increased. After all, if you go through the trouble of writing a foundational proof of safety of your code, you would rather not trust an unverified conservative garbage collector (GC) with your data. For this reason, it is very important to be able to write a type-safe GC, but the state of the art in this matter is still completely impractical since they cannot even handle cyclic data-structures. This paper’s main goals are thus:

– Show that, in order to type-check a GC that can collect cyclic data-structures, the type system has to provide a form of strong update that can change the type of a location even if the set of aliases to this location is completely unknown.

– Present a type system that provides such a facility. This type system allows the programmer to choose any mix of linear or intuitionistic typing of references and to change this choice over time to adapt it to the current needs.

– Implement the first type-preserving GC that properly collects cycles and the first generational GC that allows the mutator to use destructive assignment.

⋆ This research was sponsored in part by the Defense Advanced Research Projects Agency ISO under the title “Scaling Proof-Carrying Code to Production Compilers and Security Policies,” ARPA Order No. H559, issued under Contract No. F30602-99-1-0519, and in part by NSF Grants CCR-9901011 and CCR-0081590. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the U.S. Government.

Traditional type systems are not well-suited to reason about type-safety of low-level memory management such as explicit memory allocation, initialization, deallocation, or reuse. Existing solutions to these problems either have a very limited applicability or rely on some form of linearity constraint. Such constraints tend to be inconvenient and a lot of work has gone into relaxing them. For example, the alias types system [20] is able to cleanly handle several of the points above, even in the presence of arbitrary aliasing, as long as the aliases can be statically tracked by the type system.

The reason why it is challenging to show type-safety of low-level memory management is that for this kind of code, the line between type-safety and correctness is blurred: we end up having to prove some non-trivial properties about the code just to show its type-safety. For example, type-safety of a generational GC depends on the correct processing of the remembered-set (a data-structure holding the set of pointers from the old generation to the new).

An alternative approach would be to use Hoare logic [8] to show the correctness of the low-level code and then provide a type-safe interface to it. But it is not clear how the two would interact, especially when the low-level code might be spread over a lot of code, as is the case for the code that maintains the remembered-set in the mutator. Furthermore as we start to encode more properties into our type systems than basic typesafety, the difficulties we are seeing here will start to appear for more mundane code as well. This tendency can already be seen in the Vault project which uses an approach taken from alias-types to prove other properties of their code than just type-safety.

The present work is thus an attempt to provide a middle ground between Hoare logic and simple type-systems. Additionally to the above stated goals, we make the following contributions:

– A language that can seamlessly combine the benefits of traditional intuitionistic references and linear references at the same time.

– We introduce type cast and strong update operations that work in the absence of any static aliasing information.

– The language also offers the ability to iterate over the objects contained in a sequential area of memory.

– We show how the technique described in [16] of using the calculus of inductive constructions (CiC) as our type language to track other properties than just typesafety can be used to track properties of state.

Section 2 introduces the problem of cyclic data-structures as well as two type systems on which our work is built. Section 3 presents the problems that have pushed us to develop this system. Section 4 describes our new language. Section 5 shows how we use it to write a generational GC. We then discuss related work a conclude.

2 Background

2.1 Cyclic structures

In the course of writing the copy routine of a garbage collector, we discovered that although current type systems can handle the case where the graph is acyclic, generalizing the code to properly handle cycles proves difficult. After experimenting with various algorithms, it became clear that the problem is more fundamental: current type systems are unable to type-check generic code that can build arbitrary cyclic data-structures.

To see this, let us look at a classic example, a datatype for doubly-linked lists:

datatype α dlist = Node of α ∗ α dlist ref ∗ α dlist ref

The SML type system allows us to declare this datatype and write functions to manipulate it, but does not offer us any way to create such an object: we need a base case. So let us take another example, with a base case:

datatype α tree = Node of α | Branch of α tree ref ∗ α tree ref

This time, we can construct such trees since we do have a base case, but only if we have an object of the proper type α. More specifically, in order to create a cyclic datastructure, we always need a base case to start from, even if the data-structure we want to get in the end does not contain any node of this base case any more. Which means that a generic routine such as an unpickler or a copying GC needs to be able to construct from scratch the base case of any type that could be involved in a cyclic data-structure. In the tree example above, that means creating a Node of α for any α. Clearly this is not possible.

OCaml provides special support to build cyclic data-structures such as the dlist example above using a construct similar to val rec n = Node(0, n, n). This helps for specific code, but is of no use for generic code since it only works for pre-determined cycles, whereas a copying GC simply does not even know when it is creating cycles.

Type systems that can decouple allocation from initialization are key to solving this problem, but none of the systems developed so far are sufficiently flexible to handle the case of a generic function such as unpickle. More specifically, none of them know how to handle the case where the pointer to the allocated object escapes (i.e. is passed around and stored at arbitrary locations) before the object is initialized: when we allocate a new object, we obviously know its one and only alias, but we cannot initialize it because some of the values might not exist yet, and by the time we are done unpickling the children such that initialization can take place, there can be any number of aliases and we do not statically know them because the function is generic.

In order to type-check a practical copying GC, we need a new type system that is able to update the type (e.g. from uninitialized to initialized) of all the aliases to a particular object even when those aliases are not statically known.

2.2 Regions

Region-based type systems [18, 3] are the most practical systems offering type-safe explicit memory management. They provide a solution to the problem of safe deallocation, with a minimum of added constraints. Even though they do not offer any help when trying to type-check low-level code such as object initialization, their practicality makes them very attractive as a starting point. The idea behind region calculi is to manage memory at the level of regions (groups of objects), to annotate the type of every

(kinds) κ ::= Ω | R
(regions) ρ ::= r | ν
(types) σ ::={t | int| σ × σ | σ atρ \atop | ∀[Δ]\{Θ\}(σ⃗) → 0}

(heap type) Ψ ::= • | Ψ, ν.n ↦ σ
(type env) Γ ::= • | Γ, x:σ
(kind env) Δ ::= • | Δ, t:κ
(region env) Θ ::= • | Θ, ρ
(values)  v ::= x | i | (v, v) | ν.n | λ[Δ]{Θ}(Γ).e
(operations) op ::= v | π_{i}v | put[ρ] v | get v
(terms)  e ::= v[σ⃗](v⃗) | haltv | letx = op ine | set v := v; e | letr = newrgn ine | freergn ρ; e

Fig. 1. Syntax of a region-based language.

pointer with the region that it references, and to only provide bulk deallocation of a whole region at a time.

Figure 1 shows how such a language might look like: put[ρ] v allocates v in region ρ; get v dereferences v; newrgn creates a new region and freergn deallocates it; ν.n is a pointer to the n^{th} object in region ν created by put and has type σ at ν if the object referenced has type σ (i.e. Ψ(ν.n) = σ). Functions have type ∀[Δ]{Θ}(σ⃗) → 0; they are fully closed and we use continuation passing style, so they never return (hence the → 0 in the type); Δ is the list of type (and region) parameters; Θ lists the regions that need to be live at the time of the call; and σ⃗ lists the type of the value parameters. A function call v[σ⃗](v⃗) passes types σ⃗ and values v⃗ to function v.^{1}

Here is a sample function that creates a cyclic node of the tree datatype presented previously, assuming the language has been extended with support for datatypes:

mktree [r, t]{r}(x:t, k : ∀[r, t]{r}((tree t) atr) → 0)
= letn = put[r] (Node x) in set n := Branch n n; k[r, t](n)

The function is parameterized over type t and region r and expects an argument x of type t (which is only used temporarily to create the dummy Node) and a continuation argument k. The put operation does the allocation while the set operation does the initialization. The (omitted) kind of r is R and the kind of t is Ω. If k’s type had {} in place of {r}, it would force us to deallocate the region r before calling it and it would make n into a dangling pointer, which is allowed because liveness of the region is only needed and checked when dereferencing with get.

2.3 Alias types

The alias-types system [17, 20] was developed precisely to handle low-level code such as object initialization, memory reuse, and safe deallocation at the object level. To do that, the type of pointers is changed to carry no information about the type of the referenced object. Instead, the type of a pointer is just the location it is pointing to, so it does

1 Region calculi are not necessarily using fully closed functions and continuation passing style like we do here, but a direct-style presentation is more complex, as is the correct treatment of closure allocation.

(kinds) κ ::= Ω | Heap | Loc
(locations) ρ ::= r | ν
(types) σ ::={t | int| ν \atop | ∀[Δ]\{Θ\}(σ⃗) → 0}

(type env) Γ ::= • | Γ, x:σ
(kind env) Δ ::= • | Δ, t:κ
(mem env) Θ ::= • | Θ, ρ ↦(σ, ..., σ)
(values)  v ::= x | i | ν | λ[Δ]{Θ}(Γ).e
(operations) op ::= v | π_{i}v
(terms)  e ::= v[σ⃗](v⃗) | haltv | letx = op ine | set π_{i}v := v; e | let(r, x) = new n ine | free ρ; e

Fig. 2. Syntax of an alias-types language.

not need to change when the location’s type or liveness changes. While it provides a lot of power when dealing with low-level code, it relies on an amount of static information which is rarely available in general and definitely not available in our copying GC.

Figure 2 shows the syntax of a very simple alias-types language. It can be thought of as a region-based language where the pointers can only point to regions rather than to objects inside them and where regions have been turned into tuples. put and get have disappeared and the environment Ψ mapping locations to their types has been merged into Θ. When dereferencing a pointer of type ρ, we thus have to check the liveness and the type of the corresponding location by looking up ρ in Θ. let(r, x) = new n ine allocates a new object of size n and returns the location as both a value x and a type r. We could also have done this for regions so as to distinguish between the region type and the region value passed to put at runtime, but we conflated the two for simplicity.

Here is a sample code that takes a value of type t and creates an infinite list of this element (a 1-element circular list):

mklist [ϵ, t]{ϵ}(x : t, k:∀[ϵ, t, r]{ϵ, r ↦ (t, r)}(r) → 0)
= let(r, n) = new 2 in set π_{0}n := x; set π_{1}n := n; k[ϵ, t, r](n)

The argument ϵ has kind Heap and means that the function accepts an arbitrary heap as input, whereas the type of the continuation k shows that the returned heap is ϵ extended with a circular node at location r. Since new only knows about the size of the object, it can only do allocation and the type at location r is originally set to (int, int) and is then incrementally updated by each set operation to (t, int) and then (t, r).

The ability to update a location’s type is the key power of alias-types. But for that it relies crucially on the fact that the type system should be able to keep track of pointer values. In particular, the types need to statically but precisely describe the shape of the heap. Witness the fact in the above example that the type of the circular list is not just list t but instead explicitly describes a 1-element cycle and thus disallows any other shape. The type language of [20] is much richer than what we show here, but that does not help when the shape of the heap is simply not known statically.

2.4 Calculus of constructions

The calculus of inductive constructions (CiC) [14] that we use as our type language is an extension of the calculus of constructions (CC) [2], which is a higher-order typed logic. CC can encode Church’s higher-order predicate logic via the Curry-Howard isomorphism [9]. Understanding the details of this language is not necessary for this paper. Suffice it to say that it is a powerful typed λ-calculus where λ-terms have types of the form Πx:φ. φ which subsume both the usual arrow and the universal quantifier. Its inductive definitions are like datatypes, with elimination constructs which combine case analysis with a fixpoint operation. To know a bit more about CiC, see the appendix A.

3 Motivating example

The simple type-preserving GCs developed until now have a few important limitations. The most important one is that cyclic garbage is not properly collected. Another limitation is that generational collectors do not allow the mutator (i.e. the code that uses the GC) to create references from the old region to the young via destructive assignment. We want to lift those two restrictions, since they make those type-preserving GCs impractical.

3.1 Simple type-preserving GC

The basic idea of a type-preserving GC, proposed by Wang and Appel [22], is to layer a stop&copy collector on top of a region calculus, where the whole heap is placed in a single region and where the copy function copies the heap from the from region to a new to region and then frees the from region.

Because the type of the heap contains region annotations which will necessarily be different before copying than after, the copy function cannot just be of type t → t but instead has to be of the form M_{F} (t) → M_{T} (t) where t represents what should be preserved while the M type function annotates it with details that the mutator does not care about. Furthermore, in order to work correctly, the copy routine might require things like tag bits, mark bits or in case of generational GC it will need to make sure the mutator obeyed the generation barriers and provides a correct remembered set. All those added constraints will need to be somehow encoded in M since copy has obviously no control over t.

A good way to look at it is that t is a high-level, GC-oblivious type of the heap, while M_{F} (t) is the low-level representation with all the added details necessary for the correct functioning of the GC. The two will generally not be of the same kind; t might for example correspond to the type used in the high-level source language of the mutator code.

The simplest case is a bare-bones stop&copy GC with a source language that only supports integers and pairs. M might then look like the following, where R is the current region holding the heap:

M_{R}(int)  ⇒ int
M_{R}(τ_{1} × τ_{2}) ⇒ (M_{R}(τ_{1}) × M_{R}(τ_{2})) atR

In the case of a 2-generation collector, the heap will be spread over 2 regions: Y for the nursery and O for the old generation. M will now have to enforce that there cannot be any pointer back from O to Y by only allowing (M_{O,Y} (τ_{1}) × M_{O,Y} (τ_{2})) at Y and (M_{O,O}(τ_{1}) × M_{O,O}(τ_{2})) atO:

M_{O,A}(int)  ⇒ int
M_{O,A}(τ_{1} × τ_{2}) ⇒ ∃r ∈{O, A}.(M_{O,r}(τ_{1}) × M_{O,r}(τ_{2})) atr

In this definition, A is expected to be either equal to O or Y depending on whether pointers to Y are allowed at this place.

3.2 Generational collection

We want to create a simple yet usable type-preserving generational GC. In order to be usable, it needs to be able to properly handle cycles in the heap and it needs to allow the mutator to use destructive assignment, even if that means creating pointers back from the old generation to the nursery. The traditional way to deal with such pointers is to keep track of all of them in a remembered-set, but for simplicity, we will restrict mutability to ref-cells, as is done in SML, and place all those ref-cells in a separate region which will thus play the role of a degenerate remembered-set.

Compared to the situations outlined in the previous section, the heap is now spread over three regions: Y for the nursery, O for the old generation and R for the ref-cells. So that the collection of Y can take place without having to scan O, we need to make sure that there is no pointer from O to Y. I.e. pointers from Y and R can point to any of Y, O or R but pointers from O can only point to O or R. Our M type function which maps high-level types to their low-level representation will again have to enforce this constraint. If our high-level types include integers, ref-cells and pairs, M could be defined as follows:

M_{Y,R,O,A}(int)  ⇒ int
M_{Y,R,O,A}(ref τ) ⇒ M_{Y,R,O,Y} (τ) atR
M_{Y,R,O,A}(τ_{1} × τ_{2}) ⇒ ∃r ∈{O, A}.(M_{Y,R,O,r}(τ_{1}) × M_{Y,R,O,r}(τ_{2})) atr

Here A is expected to be either equal to O or to Y and M_{Y,R,O,A}(τ_{1} × τ_{2}) is the type of a pair that can be allocated either in O or in A and whose children (and grand-children, etc...) might also refer additionally to R or to Y.

The GC code that copies objects from the nursery Y to the old space O takes the type of the heap t, the regions Y, O, and R, and the heap itself h: M_{Y,R,O,Y} (t) as well as a continuation k. It first copies everything reachable from the root h (but only within Y) to O. Then scans all the ref-cells, considered as extra roots, and copies anything reachable from them as well. Finally, it frees Y and creates a new nursery before returning to the continuation k. It could look like the following:

GC [t:Ω^{τ}]{Y, R, O}(h:M_{Y,R,O,Y} (t), k:…)
= leth = copy[t, Y, R, O](h) in lett′, x = firstR in let = redirect[t′, Y, R, O](x) in freergn Y; letY = newrgn ink[Y, R, O](h)

where the copy function should simply do a generic deep copy, but only within the bounds of Y and the redirect function should scan the R region, redirecting any pointer to the Y region to a copy of that object in O. The type of the new root pointer h returned by copy can be described as M_{Y,R,O,O}(t).

In order to be able to free Y at the end of the collection, we need to keep track somewhere at the type-level of the fact that pointers in R that have been redirected can only point to O or to R but not to Y any more. Indeed, as the redirection is taking place the type of h keeps changing gradually until the end when it becomes equivalent to M_{O,R,O,O}(t) and thus independent from Y. If b is the boundary between what has been redirected and what has not, then we can write h:C_{Y,R,O,O,b}(t) where C is defined as:

C_{Y,R,O,A,b}(int)  ⇒ int
C_{Y,R,O,A,b}(ref τ) ⇒ letr = if(before b) O Y inC_{Y,R,O,r,b}(τ) atR
C_{Y,R,O,A,b}(τ_{1} × τ_{2}) ⇒ ∃r ∈{O, A}.(C_{Y,R,O,r,b}(τ_{1}) × C_{Y,R,O,r,b}(τ_{2})) atr

This is almost the same as the previous M, except for the added b parameter and the case of ref where the object reachable from the ref-cell will have either type C_{Y,R,O,O,b}(τ) or C_{Y,R,O,Y,b}(τ) depending on whether they have been redirected or not.

The above presentation is sloppy and simplistic but already requires unusual features from the language:

– The before b test in the definition of C_{Y,R,O,A,b}(ref τ) obviously needs to know not just the region in which the object is located but its actual location, which implies that object locations need to be reflected in the pointer type.

– The new operation first (as well as ifnext which will be needed inside redirect), that allows the code to scan the region R, should return both a new pointer x and a new type t′ where x is expected to be of type C_{Y,R,O,Y,b}(t′). But this is only safe if we know that all objects in the relevant section have a type of the form C_{Y,R,O,Y,b}(τ).

– Since the type of h, indexed by the boundary b keeps changing as the boundary moves, we need to be able to update its type when the assignment x := copy[..](..) moves the boundary, even though we do not know anything about the aliasing relationship between x and h.

The exact same three issues appear when trying to write a Cheney-style stop&copy GC where the to region is used as a queue and needs to be scanned and redirected in very similar ways.

4 Typed regions

Our new system of typed regions solves all of those problems. It can be thought of as a hybrid between alias-types and the calculus of capabilities [3] supplemented with the calculus of inductive constructions (CiC), similarly to λ_{H} [16]. Where alias-types rely on a linear map of live locations’ types and the calculus of capabilities relies on a linear set of live regions, we rely on a linear map of regions’ types.

In a typical region calculus, the type of the object reachable from a pointer (its target) is entirely given by the type of the pointer. In contrast, in the alias-types system,

(kinds) κ ::= Ω | R κ | κ → κ
(regions) ρ ::= r | ν
(types) σ, φ, τ ::={t | int| σ × σ | τ atρ.n \atop | ∀[Δ]\{Θ\}(σ⃗) → 0}

(heap type) Ψ ::= • | Ψ, ν.n ↦ τ
(type env) Γ ::= • | Γ, x:σ
(kind env) Δ ::= • | Δ, t:κ
(region env) Θ ::= • | Θ, ρ ↦(φ, n)
(values)  v ::= x | i | (v, v) | ν.n | λ[Δ]{Θ}(Γ).e
(operations) op ::= v | π_{i}v | put[ρ, τ] v | get v
(terms)  e ::= v[φ⃗](v⃗) | haltv | letx = op ine | set v :=^{φ} v; e | letr = newrgn φ ine | freergn ρ; e

Fig. 3. Syntax of the core of our language.

the type of the pointer does not provide any direct information about the type of the target; instead, the target’s type is kept in a linearly managed type map indexed by the pointer’s type, which is the singleton type holding the object’s location. Our new type system mixes the two, such that the pointer’s type holds both the location and some information (called the intended type) about the object to which it points, while the remaining information is kept in a map of regions’ types. The type of a region is a function that maps an object’s location and its intended type to its actual type.

4.1 Overview

The syntax of a trimmed down version of our language, shown in Fig. 3, looks like the simple region calculus presented before, except for the following differences:

– The region environment Θ now contains not only a list of live regions, but a map from live regions to their type φ and size n.

– Pointer types have the form τ at ρ.n rather than just σ at ρ, where n is the offset inside the region. Such a pointer does not point to an object of type τ. Instead, we force an indirection through the regions’ type such that the target’s type is Θ(ρ) n τ. Think of τ as the intended type of the location while Θ(ρ) maps those intended types to their actual value at any particular time.

– The region kind now takes a parameter κ. If ρ: R κ, then the region’s type will be of kind Nat→ κ → Ω and the term τ in τ atρ.n will have to have kind κ.

– Just as before, a value ν.n has type (Ψ(ν.n)) at ν.n but Ψ(ν.n) can now be of any kind rather than only Ω.

– put takes an additional parameter τ and returns a pointer of type τ at ρ.n after checking that v:Θ(ρ) n τ.

– set is now a strong update: it changes the type of the location to φ which has kind κ → Ω. This type needs to be provided because there are many valid choices and they are not all equivalent.

– newrgn now takes a parameter φ which is the initial type of the region.

A region’s type Θ(ρ) which ignores the location parameter n corresponds to a classical intuitionistic region system where aliases cannot be distinguished; pointer types will then typically be of the form ∃n.τ atρ.n since static tracking of n is unnecessary. On the other hand, if the type ignores the τ parameter, then it enjoys properties more like those of linear systems such as alias-types: you have to statically keep track of the exact location n, you can abstract away the intended type by using ∃t.t atρ.n, and you can change the type of a location without any regard to its previous use. The strength of our system resides in the fact that we can choose at any point from a continuum of options between those two extremes.

As mentioned, this system solves the three problems we have encountered when trying to code our generational GC: The before b test can simply compare b to the offset n of the pointer since it is now carried in its type; Since all objects in a region have a type of the form Θ(ρ) n t, setting the region’s type to something like C makes sure that first indeed returns a pointer to an object of type C(t); Finally, since Θ is managed linearly and since all memory accesses have to look up the target’s type in Θ, we can globally update the type of objects when we move the boundary by updating the corresponding type in Θ.

4.2 The language

The syntax of the full language is shown in Fig. 4. The language uses continuation passing style and fully closed functions. sort and ptm together form the pure type system corresponding to CiC. All our types are actually terms of this language and Ω is actually defined as an inductive definition in CiC. M, Ψ, Γ, Δ, Θ are environments used in the typing rules.

The region spec stored in the region environment Θ is either the type of the region together with its size (φ, n) or the set of regions for which this region can be an alias. This is used when it is not statically known into which region a reference will point, in which case, the reference will have type ∃r ∈ρ⃗.τ atr.n.

Values can be integers, pairs ((v, v) : σ × σ), references (ν.n: τ at ν.n), existential packages (⟨φ, v⟩:∃t:κ.σ), region existential packages (⟨ρ, v⟩:∃r ∈ρ⃗.σ) and functions. The terms do the following:

π_{i}v: select from a tuple. put[ρ, τ] v: allocate an object v in region ρ. get v: return the object pointed to by v. cast[P] v: safely change the type of v according to proof P. v[φ⃗](v⃗): make a tail-call to function v. haltv: halt the machine. letx:σ = op ine: bind variable x as you would expect. set v :=^{φ} v; e: do a strong update. φ describes the new type of the location. letr = newrgn φ ine: allocate a new region of type φ. freergn ρ; e: free the region ρ. cast[P] ρ ↦ φ; e: safely change the type of region ρ to φ, with proof P. let⟨t, x⟩ = open v ine: unpack the existential v into t and x. let⟨r, x⟩ = openrgn v ine: unpack the region existential v into r and x. iffirstρ (x, t . e) (e): test whether ρ is empty and selects the corresponding branch. If

non-empty, x is bound to a pointer to the first object and t to its type.

(sort)  s ::= Kind| Kscm | Ext
(ptm) φ, τ, κ, P ::= s | x | λx:φ. φ | φ φ | Πx:φ. φ | Ind(x:φ){φ⃗} | Ctor(i, φ) | Elim[φ, φ](φ){φ⃗}
(memory)  M ::= • | M, ν.n ↦ v
(heap type) Ψ ::= • | Ψ, ν.n ↦ τ
(type env)  Γ ::= • | Γ, x:σ
(kind env)  Δ ::= • | Δ, t:κ
(region env) Θ ::= • | Θ, ρ ↦θ
(region spec) θ ::= (φ, n) | ρ⃗
(regions) ρ:R κ ::= r | ν
(types)  σ:Ω ::= int| σ × σ | τ atρ.n | ∃t:κ.σ | ∃r ∈ρ⃗.σ | ∀[Δ]{Θ}(σ⃗) → 0
(values)  v ::= x | i | (v, v) | ν.n | ⟨φ, v⟩ | ⟨ρ, v⟩ | λ[Δ]{Θ}(Γ).e
(operations) op ::= v | π_{i}v | put[ρ, τ] v | get v | cast[P] v
(terms)  e ::= v[φ⃗](v⃗) | haltv | letx:σ = op ine | set v :=^{φ} v; e | letr = newrgn φ ine | freergn ρ; e | cast[P] ρ ↦ φ; e | let⟨t, x⟩ = open v ine | let⟨r, x⟩ = openrgn v ine | iffirstρ (x, t . e) (e) | ifnextv+i (x, t . e) (e)

Fig. 4. Syntax of the language

ifnextv+i (x, t . e) (e): similarly, give a pointer to the next object past v, if any. i is the size of the object pointed to by v and thus skipped by the operation.

We have decided to manipulate whole objects rather than words and not to split allocation from initialization. It is easy to change the language to provide alloc, load, and store instead of put, get, and set, but the typing rules become more verbose and so does the code in our examples.

The operational semantics of the language are shown in Fig. 5. The machine state is define as the 4-tuple (M; Θ; Ψ; e) where Θ is only used when checking the size of a region in iffirst and ifnext, and Ψ is only used to provide the type of the pointer in those same two operations. Instead of checking the size in Θ, we could look up M(ν.n) to see if it exists, which would get us rid of Θ, but that would move us further away from a realistic implementation.

The typing rules are given in the appendix, together with statements of type soundness and complete collection properties.

5 Generational collection

As suggested earlier, we will use a simple form of generational collection, so as to sidestep the issue of keeping track of the back references from the old generation to the nursery. So our source language is restricted to the following types: integers, immutable pairs, reference cells.

(M; Θ; Ψ; ν.n[\overrightarrow{φ}](\overrightarrow{v})) where M(ν.n) = λ[\overrightarrow{t:κ}]\{Θ′\}(\overrightarrow{x:σ}).e ⟹ (M; Θ; Ψ; e[φ⃗, v⃗/t⃗, x⃗])
(M; Θ; Ψ; letx = v ine)  ⟹ (M; Θ; Ψ; e[v/x])
(M; Θ; Ψ; letx = π_{i}(v_{1}, v_{2}) ine)  ⟹ (M; Θ; Ψ; e[v_{i}/x])
(M; Θ, ν ↦(φ, n); Ψ; letx = put[ν, τ] v ine)  ⟹ \begin{matrix}(M, ν.n ↦ v; Θ, ν ↦(φ, n+1); \\ Ψ, ν.n ↦ τ; e[ν.n/x]) \end{matrix}
(M; Θ; Ψ; letx = get ν.n ine)  ⟹ (M; Θ; Ψ; e[M(ν.n)/x])
(M; Θ; Ψ; letx = cast[P] v ine)  ⟹ (M; Θ; Ψ; e[v/x])
(M; Θ; Ψ; let⟨t, x⟩ = open ⟨φ, v⟩ ine) ⟹ (M; Θ; Ψ; e[φ, v/t, x])
(M; Θ; Ψ; let⟨r, x⟩ = openrgn ⟨ν, v⟩ ine) ⟹ (M; Θ; Ψ; e[ν, v/r, x])

(M; Θ; Ψ; letr = newrgn φ ine) ⟹

(M; Θ, ν ↦ (φ, 0); Ψ; e[ν/r])
where ν ∉ Dom(Θ)
(M; Θ; Ψ; freergn ν; e)  ⟹ (M\ν; Θ\ν; Ψ\ν; e)
(M; Θ, ν ↦(φ′, n); Ψ; cast[P] ν ↦ φ; e) ⟹ (M; Θ, ν ↦(φ, n); Ψ; e)
(M; Θ, ν ↦(φ′, n′); Ψ; set ν.n :=^{φ} v; e) ⟹ (M, ν.n ↦ v; Θ, ν ↦(upd φ′ n φ, n′); Ψ; e)
\begin{matrix}(M; Θ; Ψ; \\ iffirstν (x, t . e_{1}) (e_{2})) \end{matrix}  ⟹ \begin{cases}(M; Θ; Ψ; e_{2}) & if Θ(ν) = (φ, 0) \\ (M; Θ; Ψ; e_{1}[τ, ν.0/t, x]) & where Ψ(ν.0) = τ \end{cases}

(M; Θ; Ψ; ifnextν.n+i (x, t . e_{1}) (e_{2})) ⟹ \begin{cases}(M; Θ; Ψ; e_{2}) & if Θ(ν) = (φ, n+1) \\ (M; Θ; Ψ; e_{1}[τ, ν.n+1/t, x]) & where Ψ(ν.n+1) = τ \end{cases}

Fig. 5. Operational semantics of the language.

We will use three regions: O is the old generation, Y is the nursery and R contains all the ref-cells and only ref-cells. Thus R can act as a degenerate form of remembered set. We require that pointers from O can only point to O or R but not to Y.

The type of our variables have the shape M_{O,R,Y} (τ) defined below:

M_{O,R,A}(int)  ⇒ int
M_{O,R,A}(ref τ) ⇒ ∃n:Nat.τ atR.n
M_{O,R,A}(τ_{1} × τ_{2}) ⇒ ∃r ∈{O, A}.∃n:Nat.(τ_{1}, τ_{2}) atr.n

The regions’ types while the mutator is running look like:

\begin{matrix}Y ↦ & λn.λ(t_{1}, t_{2}).M_{O,R,Y} (t_{1}) × M_{O,R,Y} (t_{2}) \\ O ↦ & λn.λ(t_{1}, t_{2}).M_{O,R,O}(t_{1}) × M_{O,R,O}(t_{2}) \\ R ↦ & λn.λt.M_{O,R,Y} (t) \end{matrix}

and while a collection copying objects from Y to O is in progress and pointers in R are redirected from Y to O, the type of R is the following:

R ↦ λn.λt.letr = ifm > n then O else Y inM_{O,R,r}(t)

The top-level code of the GC code that copies objects from the nursery Y to the old space O is shown in figure 6. We omit type parameters that are obvious from context

(* Inductive definition of the source-level types. *)

InductiveΩ^{τ} : Kind:= int : Ω^{τ} | ref : Ω^{τ} → Ω^{τ} | pair : Ω^{τ} → Ω^{τ} → Ω^{τ}

(* Mapping types from source-level to low-level. *)

typedef M_{o,r,a} t = case t of int  ⇒ int | ref t  ⇒ ∃n:Nat.t atr.n | pair t_{1} t_{2} ⇒ ∃b∈{o, a}.∃n:Nat.(t_{1}, t_{2}) atb.n

(* Type of a region holding tuples, like o and y. *)

typedef TupRgn o r a = λn.λ(t_{1}, t_{2}).M_{o,r,a}(t_{1}) × M_{o,r,a}(t_{2})

(* Type of a region holding ref cells, during redirection. *)

typedef RefRgn o r y b = λn.λt.leta = if(b > n) o y inM_{o,r,a}(t)

(* Type of the continuation passed to the GC. *)

typedef gccont = ∀[y:R (Ω^{τ} × Ω^{τ})]{…}(x:M_{o,r,y}(t)) → 0

(* A deep copy function not shown here. *)

copy : ∀[t:Ω^{τ} , b:Nat, …]{…}(M_{o,r,y}(t)) → M_{o,r,o}(t)

(* Main entry point. h is the root pointer and t is its type. *)

GC [t:Ω^{τ} , …]

{y ↦ (TupRgn o r y, m_{y}), o ↦ (TupRgn o r o, m_{o}), r ↦ (λn.λt.M_{o,r,y}(t), m_{r})}
(h:M_{o,r,y}(t), k:gccont)

= leth = copy[t, 0, y, r, o](h) in iffirstr then x, t′ . redirect[t, 0, t′, y, r, o](x, h, k) else GCtail[t, y, r, o](h, k)

(* Code to execute at the end of GC when redirection is done. *)

GCtail [t:Ω^{τ} , …]

{y ↦ (TupRgn o r y, m_{y}), o ↦ (TupRgn o r o, m_{o}), r ↦ (RefRgn o r y m_{r}, m_{r})}

(h:M_{o,r,o}(t), k:gccont)

= freergn y; lety = newrgn (λ :(Ω^{τ} × Ω^{τ}). int) in cast[…] r ↦ (λn.λt.M_{o,r,y}(t)); cast[…] y ↦ (TupRgn o r y); k[y](cast[…: M_{o,r,o}(t) ◁ M_{o,r,y}(t)] h)

(* Loop through the ref cells, redirecting ptrs from y to o. *)
(* h is the root pointer that we need to pass back to GCtail. *)
(* x is the boundary pointer that sweeps through r. *)

redirect

[t:Ω^{τ} , b:Nat, t′:Ω^{τ} , …]
{y ↦ (TupRgn o r y, m_{y}), o ↦ (TupRgn o r o, m_{o}), r ↦ (RefRgn o r y b, m_{r})}
(x:t atr.b, h:M_{o,r,o}(t′), k:gccont)

= set x :=^{M_{o,r,o}} copy[t, b, y, r, o](⟨y, get x⟩); cast[…] r ↦ (RefRgn o r y (b+1)); ifnextx+1 then x, t . redirect[t, b+1, t′, y, r, o](x, h, k) else GCtail[t, y, r, o](h)

Fig. 6. Generational GC

and use direct-style rather than continuation passing style where convenient, to make the code more readable. The code of the copy function is not shown and requires additions to our language which are outside the scope of this paper.

Since the types of regions themselves refer to those regions, there is a circularity problem when we create a region that prevents us from creating the region with its proper type. In GCtail we show how to work around this problem using cast: we first create Y with a dummy type, and then cast it to the desired type (the proof needs to show that the new type preserves the type of all objects in the region; this is trivial since the region is empty). The language could allow the type of a new region to refer to that new region, but that would still not help when creating several regions whose types refer to each other.

6 Related work

The calculus of capabilities [3] was the first calculus that tried to provide safe explicit memory deallocation while allowing dangling pointers. The linear handling of our regions was strongly influenced by that work. But they did not attempt to provide any form of strong update or to solve any of the other problems related to low-level memory management.

Alias types [17, 20] also have a lot in common. In that work, strong update is the only form of update available. Separating object initialization from allocation is very easy, as is explicit deallocation and memory reuse. But the calculus keeps the notion of location abstract, preventing any reasoning on the relative position of memory objects. Also the flexibility comes at the cost of requiring a static description of all the possible aliases of the object being assigned to. This information is often simply not available.

The Vault language [4] takes the work on alias types and tries to both extend it and give it a surface syntax (so as to enable to programmer to give that needed aliasing information). In the first paper, they mostly show how to integrate classical intuitionistic references with alias-types-style statically tracked references. They also show that tracking references to region objects allows an alias-type system to subsume a region type system. The main limitation compared to our work is that you have to choose once and for all whether a reference should be intuitionistic or linear (i.e. tracked).

In the second paper [5] they try to address that limitation by introducing the notions of adoption which allows the user to make a linear reference intuitionistic, and focus which does the converse. The implementation of adoption is unclear and seems somewhat incompatible with a low-level language. As for focus, it allows some of what we want (such as strong update in the presence of arbitrary aliasing), except for the fact that the restrictions are much too severe, especially the one that requires the type change to be limited to the scope of the construct.

In the work on Typed Assembly Language [12], the authors shows a simple way to handle the problem of separating allocation from object initialization, without resorting to any form of linearity, but this approach is inherently very limited and does not seem to lend itself to any other application.

Wang and Appel [21] proposed to build a tracing garbage collector on top of a region-based calculus, thus providing both type safety and completely automatic memory management. Their type system does not support existential packages, so they have to rely on a closure conversion algorithm that represents closures as datatypes [19, 15]. This makes closures transparent, making it easy for the copy function to analyze, but it requires whole program analysis and has major drawbacks in the presence of separate compilation. More importantly, their algorithm does not address the problems linked to cycles or generations, and only presents an impractical treatment of forwarding pointers.

Monnier et al. [10] has shown how to use intensional type analysis [7] to solve the more serious problems of Wang and Appel’s work and to extend it to deal with a very primitive form of generational collection, but which does not allow cycles or even any form of destructive assignment on the part of the mutator.

Shao et al. [16] proposed to use CiC as the type calculus of programming language so as to be able to manipulate explicit proofs. We reuse their idea with the same purpose of allowing sophisticated type manipulation and arbitrary cast operations.

7 Conclusion

We have presented a novel type system that offers an unusual flexibility to play with the typing of memory locations. This type system offers the ability to choose any mix of linear or intuitionistic typing of references and to change this choice over time to adapt it to the current needs. It is able to handle strong update of memory locations even in the presence of unknown aliasing patterns. The reliance on CiC allows very sophisticated type manipulations.

We have shown how to use it to solve the difficult problem of type checking a generational garbage collector, including proper handling of cycles and while allowing the mutator to perform destructive assignment on reference cells. We have also shown how to use this same type system to encode a stack of activation records inside a region.

References

[1] A. W. Appel. Foundational proof-carrying code. In Annual Symposium on Logic in Computer Science, pages 247–258, June 2001.

[2] T. Coquand and G. P. Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.

[3] K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In Symposium on Principles of Programming Languages, pages 262–275, San Antonio, TX, Jan. 1999.

[4] R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software. In Symposium on Programming Languages Design and Implementation. ACM Press, May 2001.

[5] M. Fähndrich and R. DeLine. Adoption and focus: Practical linear types for imperative programming. In Symposium on Programming Languages Design and Implementation. ACM Press, May 2002.

[6] N. A. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni. A syntactic approach to foundational proof-carrying code. In Annual Symposium on Logic in Computer Science, pages 89–100, Copenhagen, Denmark, July 2002.

[7] B. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Symposium on Principles of Programming Languages, pages 130–141, Jan. 1995.

[8] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, Oct. 1969.

[9] W. A. Howard. The formulae-as-types notion of constructions. In To H.B.Curry: Essays on Computational Logic, Lambda Calculus and Formalism. Academic Press, 1980.

[10] S. Monnier, B. Saha, and Z. Shao. Principled scavenging. Technical Report Yale/DCS/1205, Yale University, 2000.

[11] S. Monnier and Z. Shao. Typed regions. Technical Report Yale/DCS/1242, Yale University, 2002.

[12] G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to typed assembly language. In Symposium on Principles of Programming Languages, pages 85–97, San Diego, CA, Jan. 1998.

[13] G. C. Necula. Proof-carrying code. In Symposium on Principles of Programming Languages, Jan. 1997.

[14] C. Paulin-Mohring. Inductive definitions in the system Coq—rules and properties. In M. Bezem and J. Groote, editors, Proc. TLCA. LNCS 664, Springer-Verlag, 1993.

[15] J. C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of the ACM annual conference, pages 717–740, 1972.

[16] Z. Shao, B. Saha, V. Trifonov, and N. Papaspyrou. A type system for certified binaries. In Symposium on Principles of Programming Languages, pages 217–232, Portland, OR, Jan. 2002.

[17] F. Smith, D. Walker, and G. Morrisett. Alias types. In European Symposium on Programming, 2000.

[18] M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Symposium on Principles of Programming Languages, pages 188–201, Jan. 1994.

[19] A. Tolmach and D. P. Oliva. From ML to Ada: Strongly-typed language interoperability via source translation. Journal of Functional Programming, 8(4):367–412, July 1998.

[20] D. Walker and G. Morrisett. Alias types for recursive data structures. In International Workshop on Types in Compilation, Aug. 2000.

[21] D. C. Wang and A. W. Appel. Safe garbage collection = regions + intensional type analysis. Technical Report TR-609-99, Princeton University, 1999.

[22] D. C. Wang and A. W. Appel. Type-preserving garbage collectors. In Symposium on Principles of Programming Languages, Jan. 2001.

[23] B. Werner. Une Théorie des Constructions Inductives. PhD thesis, A L’Université Paris 7, Paris, France, 1994.

(sort) s ::= Kind| Kscm | Ext
(ptm) φ ::= s | x | λx:φ. φ | φ φ | Πx:φ. φ | Ind(x:φ){φ⃗} | Ctor(i, φ) | Elim[φ, φ](φ){φ⃗}

Fig. 7. Syntax of the calculus of inductive constructions.

A Calculus of constructions

The syntax of CiC is shown in Fig 7. The λ term corresponds to the abstraction of the λcalculus, and the Π term is a dependent product type. When the bound variable does not occur in the body, the product type is usually abbreviated as φ → φ. In the terminology of pure type systems, Kind, Kscm, and Extare the sorts.

CiC, as its name implies, extends the calculus of constructions with inductive definitions. An inductive definition can be written in a syntax similar to that of ML datatypes. For example, the following introduces an inductive definition of polymorphic lists:

Ind(List:Kind→ Kind){nil : Πx.List x | cons : Πx.x → List x → List x}

The logic also provides elimination constructs for inductive definitions, which combine case analysis with a fixpoint operation. Objects of an inductive type can thus be iterated over using these constructs. In order for the induction to be well-founded and for iterators to terminate, a few constraints are imposed on the shape of inductive definitions; most importantly, the defined type can only occur positively in the arguments of its constructors.The calculus of inductive constructions has been shown to be strongly normalizing [23], hence the corresponding logic is consistent.

In the remainder of this paper, we will use more familiar mathematical notation , rather than the strict definition of CiC syntax given in this section. For example, inductive definitions will be presented in BNF format. We will, however, retain the Π notation, which can generally be read as a universal quantifier.

B Typing rules

The typing rules for the terms of our language are given here in Fig. 9 and 10. Those rules use the two following auxiliary type functions:

upd φ n φ′ = λm.λt.if(m = n) (φ′ t) (φ m t)
size(σ_{1} × σ_{2}) ⇒ size(σ_{1}) + size(σ_{2})
size(∃t:κ.σ) ⇒ size(σ)
size(∃r ∈ρ⃗.σ) ⇒ size(σ)
size( )  ⇒ 1

The main judgments are:

– Ψ; Δ; Θ; Γ ⊢ v : σ if v has type σ in the given environment.

– Ψ; Δ; Θ; Γ ⊢ e if e is well-formed under the given environment.

[figure]

⊢ Δ  Δ ⊢ Γ  ⊢ Ψ  Δ ⊢ Θ  Ψ; Θ ⊢ M
\overline{⊢ •}  \frac{⊢ Δ  Δ ⊢ t : κ}{⊢ Δ, t:κ}  \frac{Δ ⊢ σ_{i} : Ω}{Δ ⊢ x_{0} :σ_{0}, …, x_{n}:σ_{n}}

\frac{• ⊢ φ_{ij} : κ  • ⊢ ν_{i} : R κ}{⊢ ν_{0}.0 ↦ φ_{00}, …, ν_{m}.n ↦ φ_{mn}}  \frac{Δ ⊢ ρ_{i} ↦θ_{i}}{Δ ⊢ ρ_{0} ↦ θ_{0}, …, ρ_{n} ↦ θ_{n}}

\frac{Δ ⊢ ρ : R κ  Δ ⊢ ρ_{i} : R κ}{Δ ⊢ ρ↦ρ⃗}  \frac{Δ ⊢ ρ : R κ  Δ ⊢ φ : Nat → κ → Ω}{Δ ⊢ ρ ↦(φ, n)}

\frac{∀j:0..n_{i}−1 . Ψ; •; •; • ⊢ M(ν_{i}.j) : φ_{i} j (Ψ(ν_{i}.j))}{Ψ; ν_{0} ↦ (φ_{0}, n_{0}), …, ν_{n} ↦ (φ_{n}, n_{n}) ⊢ M}  \frac{Ψ; Θ ⊢ M  Ψ; Θ; •; • ⊢ e}{⊢ (M; Θ; Ψ; e)}

Fig. 8. Environment formation rules.

– Ψ; Δ; Θ; Γ ⊢ v ↦ σ if v points to an object of type σ.

– σ ◁ σ′ if σ is a subtype of σ′.

– Θ ⊢ ρ ∈ ρ⃗ if ρ is indeed one of ρ⃗.

– Θ ⊢ Θ′ if Θ′ can be used in lieu of Θ because it contains the same regions with the same types (but they can differ w.r.t. to region aliases).

The typing rules for environments are given in Fig. 8 together with the definition of a well-formed machine state ⊢ (M; Θ; Ψ; e).

B.1 Properties of the language

We state here a few lemmas used in the proof of type soundness. The proofs can be found in the companion technical report [11]. Since our type language is CiC, we know it is strongly normalizing and confluent.

The proofs of the lemmas below do not present any unusual difficulty, contrary to what was the case in [10] where the widen operator introduced a lot of extra trouble. The substitution lemma for types turned out to be simpler than expected when substituting ν for r in a Θ such as {r ↦ν, ν ↦…}.

One annoyance is that Ψ; Δ; Θ; Γ ⊢ v : σ has to be re-proven each time Θ is changed. Luckily, reconstructing the new proof is simple since Θ is only used in those rules in order to verify that the witness of a package of type ∃r ∈ρ⃗.σ is indeed in ρ⃗.

Lemma 1 (Subsumption). If σ ◁ σ′ and Ψ; Δ; Θ; Γ ⊢ v : σ then Ψ; Δ; Θ; Γ ⊢ v : σ′.

Lemma 2 (Deallocation). If Ψ; Δ; Θ; Γ ⊢ e and ρ ∉ Dom(Θ) then Ψ\ρ; Δ; Θ; Γ ⊢ e.

Lemma 3 (Substitution). If Ψ; Δ; Θ; Γ ⊢ v : σ then:

– If Ψ; Δ; Θ; Γ{x:σ} ⊢ v′ : σ′ then Ψ; Δ; Θ; Γ ⊢ v′[v/x] : σ′.

[figure: Ψ; Δ; Θ; Γ ⊢ e]

\frac{Ψ; Δ; Θ; Γ ⊢ v ↦ ∀[\overrightarrow{t:κ}]\{Θ′\}(σ⃗) → 0 • ⊢ σ⃗ : \overrightarrow{t:κ}  Θ ⊢ Θ′[σ⃗/t⃗]  Ψ; Δ; Θ; Γ ⊢ v_{i} : σ_{i}[σ⃗/t⃗]}{Ψ; Δ; Θ; Γ ⊢ v[σ⃗](v⃗)}

Ψ; Δ; •; Γ ⊢ v : int Ψ; Δ; •; Γ ⊢ haltv

\frac{Ψ; Δ; Θ; Γ ⊢ v : φ n τ Ψ; Δ; Θ, ρ ↦(φ, n+1); Γ, x:τ atρ.n ⊢ e}{Ψ; Δ; Θ, ρ ↦(φ, n); Γ ⊢ letx = put[ρ, τ] v ine}

\frac{Ψ; Δ; Θ; Γ ⊢ op : σ  Ψ; Δ; Θ; Γ, x:σ ⊢ e}{Ψ; Δ; Θ; Γ ⊢ letx:σ = op ine}  \frac{Ψ; Δ; Θ; Γ ⊢ e}{Ψ; Δ; Θ, ρ↦(φ, n); Γ ⊢ freergn ρ; e}
\frac{Ψ; Δ; Θ, ρ↦(φ′, n); Γ ⊢ e  Δ ⊢ ρ : R κ Δ ⊢ P : Πi:0..n−1. Πt:κ. (φ i t) ◁ (φ′ i t)}{Ψ; Δ; Θ, ρ↦(φ, n); Γ ⊢ cast[P] ρ ↦ φ′; e}  \frac{Δ ⊢ φ : Nat → κ → Ω Ψ; Δ, r:R κ; Θ, r ↦(φ, 0); Γ ⊢ e}{Ψ; Δ; Θ; Γ ⊢ letr = newrgn φ ine}

\frac{Ψ; Δ; Θ, ρ↦(φ, n); Γ ⊢ v : τ atρ.m Ψ; Δ; Θ, ρ↦(φ, n); Γ ⊢ v′ : φ′ τ size(φ′ τ) = size(φ m τ) Ψ; Δ; Θ, ρ↦(upd φ m φ′, n); Γ ⊢ e}{Ψ; Δ; Θ, ρ↦(φ, n); Γ ⊢ set v :=^{φ′} v′; e}

\frac{Ψ; Δ; Θ; Γ ⊢ v : ∃r′ ∈ρ⃗.σ  Δ ⊢ ρ_{i} : R κ Ψ; Δ, r:R κ; Θ, r ↦ρ⃗; Γ, x:σ[r/r′] ⊢ e}{Ψ; Δ; Θ; Γ ⊢ let⟨r, x⟩ = openrgn v ine}  \frac{Ψ; Δ; Θ; Γ ⊢ v : ∃t′:κ.σ Ψ; Δ, t:κ; Θ; Γ, x:σ[t/t′] ⊢ e}{Ψ; Δ; Θ; Γ ⊢ let⟨t, x⟩ = open v ine}

\frac{Δ ⊢ ρ : R κ Ψ; Δ; Θ, ρ ↦(φ, 0); Γ ⊢ e_{2} Ψ; Δ, t:κ; Θ, ρ ↦(φ, n); Γ, x:t atρ.0 ⊢ e_{1}}{Ψ; Δ; Θ, ρ ↦(φ, n); Γ ⊢ iffirstρ (x, t . e_{1}) (e_{2})}

\frac{Ψ; Δ; Θ; Γ ⊢ v ↦ σ  i = size σ Ψ; Δ; Θ; Γ ⊢ v : τ atρ.m  Ψ; Δ; Θ, ρ ↦(φ, m+1); Γ ⊢ e_{2} Δ ⊢ ρ : R κ  Ψ; Δ, t:κ; Θ, ρ ↦(φ, n); Γ, x:t atρ.m+1 ⊢ e_{1}}{Ψ; Δ; Θ, ρ ↦(φ, n); Γ ⊢ ifnextv+i (x, t . e_{1}) (e_{2})}

Fig. 9. Static semantics of the language.

– If Ψ; Δ; Θ; Γ{x:σ} ⊢ e then Ψ; Δ; Θ; Γ ⊢ e[v/x]. If Δ ⊢ φ : κ then:

– If Ψ; Δ{t:κ}; Θ; Γ ⊢ v : σ then Ψ; Δ[φ/t]; Θ[φ/t]; Γ[φ/t] ⊢ v[φ/t] : σ[φ/t].

– If Ψ; Δ{t:κ}; Θ; Γ ⊢ e then Ψ; Δ[φ/t]; Θ[φ/t]; Γ[φ/t] ⊢ e[φ/t]. Lemma 4 (Type Preservation). If ⊢ (M; Θ; Ψ; e) and (M; Θ; Ψ; e) ⟹ (M′; Θ′; Ψ′; e′) then ⊢ (M′; Θ′; Ψ′; e′).

[figure: Ψ; Δ; Θ; Γ ⊢ v : σ]

\overline{Ψ; Δ; Θ; Γ ⊢ n : int} \overline{Ψ; Δ; Θ; Γ ⊢ x : Γ(x)}  \frac{Ψ; Δ; Θ; Γ ⊢ v_{i} : σ_{i}}{Ψ; Δ; Θ; Γ ⊢ (v_{1}, v_{2}) : σ_{1} × σ_{2}}

\frac{ν.n ∈ Dom(Ψ) ⇒ τ = Ψ(ν.n)}{Ψ; Δ; Θ; Γ ⊢ ν.n : τ atν.n}  \frac{Ψ; Δ; Θ; \overrightarrow{x:σ} ⊢ e}{Ψ; Δ′; Θ′; Γ ⊢ λ[Δ]\{Θ\}(\overrightarrow{x:σ}).e : ∀[Δ]\{Θ\}(σ⃗) → 0}

\frac{Δ ⊢ φ : κ  Ψ; Δ; Θ; Γ ⊢ v : σ[φ/t]}{Ψ; Δ; Θ; Γ ⊢ ⟨φ, v⟩ : ∃t:κ.σ}  \frac{Ψ; Δ; Θ; Γ ⊢ v : σ[ρ/r] Δ ⊢ ρ : R κ  Δ ⊢ ρ_{i} : R κ  Θ ⊢ ρ ∈ ρ⃗}{Ψ; Δ; Θ; Γ ⊢ ⟨ρ, v⟩ : ∃r ∈ρ⃗.σ}

[figure]

Θ ⊢ ρ ∈ ρ⃗  Ψ; Δ; Θ; Γ ⊢ v ↦ σ  Ψ; Δ; Θ; Γ ⊢ op : σ

\frac{ρ ∈ ρ⃗}{Θ ⊢ ρ ∈ ρ⃗}  \frac{Θ ⊢ ρ_{i} ∈ ρ⃗′}{Θ, ρ↦ρ⃗ ⊢ ρ ∈ ρ⃗′}  \frac{Θ(ρ) = (φ, m)}{Θ ⊢ τ atρ.n ↦ φ n τ}  \frac{Θ ⊢ τ atρ_{i}.n ↦ σ[ρ_{i}/ρ]}{Θ, ρ↦ρ⃗ ⊢ τ atρ.n ↦ σ}

\frac{Ψ; Δ; Θ; Γ ⊢ v : τ atρ.n  Θ ⊢ τ atρ.n ↦ σ}{Ψ; Δ; Θ; Γ ⊢ v ↦ σ}  \frac{Ψ; Δ; Θ; Γ ⊢ v ↦ σ}{Ψ; Δ; Θ; Γ ⊢ get v : σ}

\frac{Ψ; Δ; Θ; Γ ⊢ v : σ_{1} × σ_{2}}{Ψ; Δ; Θ; Γ ⊢ π_{i}v : σ_{i}}  \frac{Ψ; Δ; Θ; Γ ⊢ v : σ′  Δ ⊢ P : σ′ ◁ σ}{Ψ; Δ; Θ; Γ ⊢ cast[P] v : σ}

[figure] Θ ⊢^{live} ρ  Δ ⊢ σ⃗ : t⃗:κ  Θ ⊢ Θ′  σ ◁ σ′

\overline{Θ, ρ↦(φ, n) ⊢^{live} ρ}  \frac{Θ ⊢^{live} ρ_{i}}{Θ, ρ↦ρ⃗ ⊢^{live} ρ}  \frac{Δ ⊢ σ : κ  Δ ⊢ σ⃗ : \overrightarrow{t:κ}[σ/t]}{Δ ⊢ σ, σ⃗ : t:κ, \overrightarrow{t:κ}}

\overline{Θ ⊢ Θ}  \frac{Θ ⊢ Θ′}{Θ, ρ ↦(φ, n) ⊢ Θ′, ρ ↦(φ, n)}  \frac{Θ ⊢ Θ′  Θ ⊢ ρ ∈ ρ⃗′}{Θ ⊢ Θ′, ρ ↦ρ⃗′}  \frac{Θ ⊢ Θ′}{Θ, ρ↦ρ⃗′ ⊢ Θ′}

\overline{σ ◁ σ}  \frac{σ_{1} ◁ σ′_{1}  σ_{2} ◁ σ′_{2}}{σ_{1} × σ_{2} ◁ σ′_{1} × σ′_{2}}  \frac{ρ⃗ ⊂ ρ⃗′  σ ◁ σ′}{∃r ∈ρ⃗.σ ◁ ∃r ∈ρ⃗′.σ′}

Fig. 10. Typing values and operations, with auxiliary rules.

Lemma 5 (Progress). If ⊢ (M; Θ; Ψ; e) then either e = halt v or there exists a state (M′; Θ′; Ψ′; e′) such that (M; Θ; Ψ; e) ⟹ (M′; Θ′; Ψ′; e′).

Lemma 6 (Complete Collection). If ⊢ (M; Θ; Ψ; e) and (M; Θ; Ψ; e) ⟹^{∗} (M′; Θ′; Ψ′; e′) and ∀ν.n ∈ Dom(M) . ν ∈ Dom(Θ) then ∀ν.n ∈ Dom(M′) . ν ∈ Dom(Θ′). In particular, if e′ = haltv then M′ = •.