Principled Scavenging^{∗}

Stefan Monnier  Bratin Saha  Zhong Shao

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

{monnier, saha, shao}@cs.yale.edu

YALEU/DCS/TR-1205 November 2000

Abstract

Proof-carrying code and typed assembly languages aim to minimize the trusted computing base by directly certifying the actual machine code. Unfortunately, these systems cannot get rid of the dependency on a trusted garbage collector. Indeed, constructing a provably type-safe garbage collector is one of the major open problems in the area of certifying compilation.

Building on an idea by Wang and Appel, we present a series of new techniques for writing type-safe stop-and-copy garbage collectors. We show how to use intensional type analysis to capture the contract between the mutator and the collector, and how the same method can be applied to support forwarding pointers and generations. Unlike Wang and Appel (which requires whole-program analysis), our new framework directly supports higher-order funtions and is compatible with separate compilation; our collectors are written in provably type-safe languages with rigorous semantics and fully formalized soundness proofs.

1. Introduction

The correctness of most type-safe systems relies critically on the correctness of an underlying garbage collector (GC). This also holds for Proof-Carrying Code (PCC) [13] and Typed Assembly Languages (TAL) [12]—both of which aim to minimize the trusted computing base (TCB) by directly certifying the actual machine code. Unfortunately, these systems cannot get rid of the dependency on a trusted GC. Indeed, constructing a verifiably type-safe GC is widely considered as one of the major open problems in the area of certifying compilation [11, 3].

Recently, Wang and Appel [23] proposed to tackle the problem by building a tracing garbage collector on top of a region-based calculus. Our work builds on theirs but makes the following new contributions:

• We show how to use intensional type analysis (ITA) [19, 8] to accurately describe the contract between the mutator and the collector and how the same framework can be applied to construct various different type-safe GCs.

• Using ITA to typecheck GC may seem to be an obvious idea (at least to some people), however, none of the previous work [21, 15, 19] have succeeded in getting it to work. Indeed, Wang and Appel [23] subsequently gave up on using ITA. We show why the problem is nontrivial (see Section 2.2) and how to modify the basic ITA framework to solve the problem.

• Wang and Appel’s collector [23] relies on whole-program analysis and code duplication to support higher-order and polymorphic languages—this breaks separate compilation and is impractical. We show how to use runtime type analysis to write our GC as a library (thus no code duplication) and how to directly support higher-order functions and polymorphism.

• We expose in detail how to implement and certify efficient forwarding pointers. Making them type-safe is surprisingly subtle (see Section 7). Wang and Appel [23] also claim to support forwarding pointers but their scheme is less efficient and it is unclear whether it is sound.

• We also show how to handle generations with a simple extension of our base calculus.

• A garbage collector is type-safe only if it is written in a provably type-safe language. We have complete type-soundness proofs for all our calculi (see Appendix).Wang and Appel’s collectors [23, 22], on the other hand, are not fully formalized.

Although our paper is theoretical in nature, we believe it will be of great interests to the general audience, especially those who are looking to apply new language theory to solve important practical problems such as mobile-code safety and certifying compilation. We have started implementing our type-safe GCs in the FLINT system [16], however, making the implementation realistic still involves solving the remaining problems (e.g., breadth-first copying, remembered sets, and data structures with cycles, which we still cannot support satisfactorily) thus is beyond the scope of this paper. Nevertheless, we believe our current contributions constitute a significant step towards the goal of providing a practical type-safe garbage collector.

2. Motivation and background

Why do we want a type-safe garbage collector?

∗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.

The explosive growth of the Internet has induced newfound interest in mobile computation as well as security. Increasingly, applications are being developed at remote sites and then downloaded for execution. A robust mobile code system must allow code from potentially untrusted sources to be executed. At the same time, the system must detect and prevent the execution of malicious code.

The safety of such a system depends not only on the properties of the code being downloaded, but also on the security of the host system itself, or more specifically, its trusted computing base (TCB).

Proof-carrying code [13] and typed assembly languages [12] have been proposed to reduce the size of this TCB by bundling the untrusted code with a mechanically checkable proof of safety, where the safety is usually defined as type-safety. Such systems only need to trust their verifier and runtime system rather than their whole compiler suite.

But all these certifying-compiler projects (e.g., PCC, TAL) still crucially rely on the correctness of a tracing garbage collector for their safety. Recently, both Crary [3] and Morrisett [11] have characterized type-safe garbage collection as one of the major open problems in the area of certifying compilation.

A type-safe GC is not only desirable for reducing the size of the TCB but also for making it possible to ship custom-tailored GC along with mobile code, or to choose between many more GC variants without risking the integrity of the system. Writing GC inside a type-safe language itself also makes it possible to achieve principled interoperation between garbage collection and other memorymanagement mechanisms (e.g., those based on malloc-free and regions). Indeed, one major software-engineering benefit is that a type-safe GC must make explicit the contract between the collector and the mutator and it must make sure that it is always respected. Without typechecking, such rules can prove difficult to implement correctly and bugs can be very difficult to find.

2.1 The problem

Recently, Wang and Appel [21] proposed to tackle the problem by layering a stop-and-copy tracing garbage collector [24] on top of a region based calculus, thus providing both type safety and completely automatic memory management.

A region calculus [17] annotates the type of every heap object with the region in which it is allocated (such as σ_{1} ×^{ρ} σ_{2} where ρ is the region), and thus allows to safely reclaim memory by freeing a whole region if that region does not appear in any of the currently live types.

The basic idea in building a type-safe GC is to concentrate on type-safety rather than correctness. Rather than try to prove that the copy function faithfully copies all the heap, we just need to show that it has a type looking somewhat like ∀α.(α → (α[T/F])) where (α[T/F]) stands for the type α where the region annotation T is substituted for F(see Fig. 1). Assuming we have such a function and we don’t keep any reference to the region F, the region calculus will allow us to safely reclaim F.

Clearly, there is no correctness guarantee in sight since the value returned by that copy function might have a completely different value or might not faithfully reproduce the original graph, but it ensures type-safe execution of the whole mutator-collector system and even offers a form of type-preservation guarantee.

The main problem is clearly to write this copy function which needs to trace through arbitrary heap structures at runtime. Therefore, the language needs to support some form of runtime type information in order to do the actual copy.

In their followup paper [23], Wang and Appel suggest to circumvent the problem of runtime type information using a mix of

[figure: F; ⋮; ×^{F}; ⋮; ×^{F}; int; int; int; ⇒; T; ⋮; ×^{T}; ⋮; ×^{T}; int; int; int]
copy : ∀F.∀T.∀α.(α ⟶ α[T/F])
GC = ΛF.Λα.λ(x:α, k:∀ρ.α[ρ/F] → 0)
letregion Tin

lety = copy[F][T][α](x) in only Tink[T](y)

Figure 1: Stop-and-Copy from region F to region T.

GC is written in continuation passing style (CPS). It takes the current region, the heap and a continuation and begins by allocating a new region T with “let region T in e”. It then copies the heap into this new region and then frees the old region implicitly with “onlyTine” which tells the region management that all regions but Tcan be reclaimed. This way of freeing regions was introduced by Wang and Appel to circumvent problems linked to aliasing of regions.

monomorphization and defunctionalization (a form of closure conversion due to Tolmach [18]) to simplify the problem to a monomorphic first order calculus. However, this approach suffers from several major drawbacks:

• Most importantly, it is not generally applicable and requires whole program analysis which rule out separate compilation.

• It can introduce a significant code size increase and forces the use of separate specialized GC and copy functions for each type appearing in the program. Instead of the promised flexibility to choose among various GC variants, this approach locks you into a single 100% tailor made collector.

• Finally, although their type-safe GC does properly formalize the interaction between the mutator and the collector, the formalization is hidden inside the compiler and hence does not allow to bring out open the overly intimate relationship between the GC and the compiler.

They also try to preserve sharing using forwarding pointers. The rough sketch of the solution they propose is similar to the one we developed (which is done independently). It relies mostly on a very powerful form of cast which allows some amount of covariant subtyping of references. Making sure that this cast is sufficiently constrained to be safe is difficult. Their informal presentation is incomplete and possibly incorrect, and leaves many important questions unanswered.

2.2 Our solution

We want to do away with any form of whole program analysis so as to make the mutator and the collector independent in order to reap the promised benefits of more flexibility and clearer interaction between mutator and GC.

In this paper, we present a different approach for writing the copy function, relying on runtime type analysis. The return type of copy (α[T/F], a form of Typerec) as well as the need to observe types at runtime leads one very naturally to use intensional type analysis (ITA). In fact, an early paper of Wang and Appel [21] was titled “safe garbage collection = regions + intensional type analysis;” but they failed to make it work, and they subsequently gave up on using ITA and ended up opting for the lower-tech solution mentioned above [23]. Saha et al. [15, 19] also tried to use ITA to write the copy function, but their attempt is missing crucial details and didn’t really work either.

2.2.1 A case for symmetry

So what is the problem? It seems that ITA provides us with just the right tools. We can for example write a simple Typerec such as S_{T,F}(σ) which substitutes Tfor F and then use typecase in the body of copy.

But that means that the type grows each time we go through the GC, from σ to S_{T,F}(σ) to S_{ρ,T}(S_{T,F}(σ)) …. This may seem unimportant since S should be reduced away anyway. But S_{ρ,T}(α) cannot be reduced further until α is instantiated: ∃α.S_{T,F}(α) is a normal form. So the accumulation of S operators is a real problem, since S_{ρ,F}(α) is not equal to S_{ρ,T}(S_{T,F}(α)).

We could arrange for S_{ρ,T}(S_{T,F}(σ)) to reduce to S_{ρ,F}(σ). But then all types become S_{ρ,F}(σ) (where F is the “initial region”) except before the first collection. Also it is very ad-hoc and only works as long as S is a quasi-identity.

A better approach is to ensure that the input and output types are symmetric. We first redefine S_{ρ}(σ) which simply substitutes ρ for any region annotation (why bother with an initial region) and then redefine copy to have type ∀F.∀T.∀α.(S_{F}(α) → S_{T}(α)) which gets us rid of the special case before the first collection and does not require any special reduction rule for S since GC does not increase the size of the type any more.

2.2.2 A case for tags

The above solution looks good until we try to copy an existential package ∃α:{F}.S_{F}(α) to ∃α:{T}.S_{T}(α).

Type variables hide region annotations, so we need to annotate their kinds with the relevant region information. We write it “α : Δ” to mean that α can only range over types that refer exclusively to the regions included in Δ.

So, by opening the existential package, we can get the value σ of α and the value of type S_{F}(σ), and a recursive call to copy will return S_{T}(σ), but how can we construct the new existential package ? Reusing σ as-is will not do since σ is not constrained to {T} but to {F}. We would want to use S_{T}(σ) but that cannot work either; the only correctly typed package we can produce is ⟨α=S_{T}(σ), v:α⟩ which has type ∃α:{T}.α.

We are again pushing a new S onto the type rather than replacing an S with another. So we can again arrange for S_{T}(S_{F}(σ)) to reduce to S_{T}(σ), but we really do not want to tie our hands with such an ad-hoc and restrictive scheme.

Instead, we can pay a bit more attention to what we do and observe that S_{ρ}(σ) makes region annotations on σ completely useless, so instead of trying to get those annotations right only to see them substituted we can simply define a parallel set of nonannotated types τ (that we will call tags). Since tags have no region annotations, we can hide them in tag variables without any Δ constraint, which side-steps the problem of copying existentials conveniently.

Such a split between types and tags is not a new concept since it was already used in the work on intensional type analysis where tags were called constructors [8, 5]. But here, tags take on more significance since they correspond to a source-level notion of type and will be mapped to different actual types with different type functions M (formerly S) which are used to encapsulate all the constraints that mutator data has to satisfy in order for the collector to do its job. As you will see in sections 7 and 8 we will use a non-trivial M mapping to force the mutator to provide space for forwarding pointers and to enforce the invariant that references do not point from the old generation to the new.

3. Source language λ_{CLOS}

For simplicity of the presentation, the source language we propose to compile and garbage collect is the simply typed λ-calculus. In order to be able to use our region calculus, we need to convert the source program into a continuation passing style form (CPS). And we also need to close our code to make all data manipulation explicit, so we turn all closures into existential packages.

We won’t go into the details of how to CPS convert that source language [7]. Similarly, for the closure conversion using existentials [10, 9].

The language used after CPS conversion and closure conversion is the language λ_{CLOS} shown below.

(types)  τ ::= Int| t | τ_{1} × τ_{2} | τ → 0 | ∃t.τ
(values)  v ::= n | f | x | (v_{1}, v_{2}) | ⟨t=τ_{1}, v:τ_{2}⟩
(terms)  e ::= letx = v ine | letx = π_{i}v ine | v_{1}(v_{2}) | open v as ⟨t, x⟩ ine | haltv
(programs) p ::= letrec \overrightarrow{f = λ(x:τ).e} ine

Since functions are in CPS, they never return, which we represent with the arbitrary return type 0. To represent closures, the language includes existential packages constructed by ⟨t=τ_{1}, v:τ_{2}⟩ and of type (∃t.τ_{2}). The open v as ⟨t, x⟩ in e construct takes an existential package v, binds the witness type to t and the value to x, and then executes e. The complete program consists of a list of mutually recursive closed function declarations followed by the main term to be executed.

4. Target language λ_{GC}

The language used to write the garbage-collector (and into which we translate λ_{CLOS} programs) is shown in Fig. 2. It extends λ_{CLOS} with regions [17] and intensional type analysis [8, 19]. Functions are also fully closed and use CPS but they can additionally be polymorphic over tags and regions.

4.1 Regions

Our region calculus uses “references” denoted ν.ℓ of type (σ atρ) rather than annotations like σ_{1}×^{ρ}σ_{2} (which is written (σ_{1} × σ_{2}) atρ instead). Similarly, object allocation and memory accesses are made explicit with put and get. This was only preferred because of its orthogonality.

Region allocation and reclamation is done with let region and only. Deallocation of a region is implicit since onlylists the regions that should be kept. This neatly works around aliasing problems, at the cost of a more expensive deallocation operation (only needs to go through the list of all regions to find which ones need to be reclaimed). In our case, we have very few regions and deallocate them only occasionally, so it is a good tradeoff.

(tenv)  Θ ::= · | Θ, t:κ
(venv)  Γ ::= · | Γ, x:σ
(renv)  Δ ::= · | Δ, ρ
(α env)  Φ ::= · | Φ, α:Δ
(region types) Υ ::= {ℓ_{1} :σ_{1}, …, ℓ_{n}:σ_{n}}
(mem types) Ψ ::= {cd:Υcd, ν_{1} :Υ_{1}, …, ν_{n}:Υ_{n}}
(regions)  R ::= {ℓ_{1} ↦ v_{1}, …, ℓ_{n} ↦ v_{n}}
(memories) M ::= {cd ↦ Rcd, ν_{1} ↦ R_{1}, …, ν_{n} ↦ R_{n}}
(states)  P ::= (M, e)
(regions)  ρ ::= ν | r
(kinds)  κ ::= Ω | Ω ⟶ Ω
(tags)  τ ::={t | Int| τ_{1} × τ_{2} | τ → 0 | ∃t.τ \atop | λt.τ | τ_{1}τ_{2}}
(types)  σ ::= int| σ_{1} × σ_{2} | ∀[t⃗:κ][r⃗](σ⃗) → 0 ; | ∃t:κ.σ | σ atρ | M_{ρ}(τ) | α ; | ∀⟦τ⃗⟧[r⃗](σ⃗) ⟶^{ρ} 0 | ∃α:Δ.σ

(values)  v ::={n | x | ν.ℓ | (v_{1}, v_{2}) | ⟨t=τ, v:σ⟩ | v⟦τ⃗⟧ \atop | ⟨α:Δ=σ_{1}, v:σ_{2}⟩ | λ[t⃗:κ][r⃗](\overrightarrow{x:σ}).e}
(operations) op ::= v | π_{i}v | put[ρ]v | get v
(terms)  e ::= v[τ⃗][ρ⃗](v⃗) | letx = op ine | haltv | ifgc ρ e_{1} e_{2} | open v as ⟨t, x⟩ ine | open v as ⟨α, x⟩ ine | letregion r ine | only Δ ine | typecase τ of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃})

(tagnf)  τ′ ::={t| Int| τ′ → 0 | τ′_{1} × τ′_{2} | ∃t.τ′ | λt.τ′ \atop | tτ′}

Figure 2: Syntax of λ_{GC}

4.2 Intensional type analysis

As explained earlier, we have split the notion of type into two. Tags represent the runtime type descriptors and map very directly to source-level types without any region annotations. The only different between λ_{CLOS} types and λ_{GC} tags is the addition of tag functions λt.τ and tag applications τ_{1}τ_{2}, which are needed for type analysis of existentials [19]. To do the actual analysis of tags, terms include a refining typecase construct, i.e. a more refined tag is substituted for τ in each arm of the typecase . Finally, instead of a full-blown Typerec construct we only provide a hard coded M, to keep the presentation simpler. M_{ρ}(τ) is the type corresponding to the tag τ complemented with region annotations ρ:

M_{ρ}(Int)  ⟹ int
M_{ρ}(τ_{1} × τ_{2}) ⟹ (M_{ρ}(τ_{1}) × M_{ρ}(τ_{2})) atρ
M_{ρ}(∃t.τ) ⟹ (∃t:Ω.M_{ρ}(τ)) atρ
M_{ρ}(τ → 0) ⟹ ∀[][r](M_{r}(τ)) → 0 atcd

This definition of Mforces the mutator to maintain the invariant that all objects are allocated in the same region, which is all our garbage collector requires.

4.3 Functions and code

Since programs in λ_{GC} are completely closed, we can separate code from data. The memory configuration enforces this by having a separate dedicated region cd for code blocks. The indirection provided by memory references allows us to do away with letrec. A value λ[t⃗][r⃗](\overrightarrow{x:σ}).e is only an array of instructions (which can contain references to other values in cd) and needs to be putinto a region to get a function pointer before one can call it. In practice,

[figure: F ⊢ λ_{CLOS} ⇒ λ_{GC}]

F ⊢_{v} n ⇒ n  F ⊢_{v} f ⇒ cd.F (f)  F ⊢_{v} x ⇒ x

\begin{matrix}F ⊢_{v} v_{1} ⇒ v′_{1} & F ⊢_{v} v_{2} ⇒ v′_{2} \\ F ⊢_{v} (v_{1}, v_{2}) ⇒ put[r](v′_{1}, v′_{2}) \end{matrix}

{F ⊢_{v} v ⇒ v′ \atop F ⊢_{v} ⟨t=τ_{1}, v:τ_{2}⟩ ⇒ put[r]⟨t=τ_{1}, v′:M_{r}(τ_{2})⟩}

\begin{matrix}F ⊢_{v} v_{1} ⇒ v′_{1} & F ⊢_{v} v_{2} ⇒ v′_{2} \\ F ⊢_{e} v_{1}(v_{2}) ⇒ v′_{1}[][r](v′_{2}) \end{matrix} F ⊢_{v} v ⇒ v′

F ⊢_{e} haltv ⇒ haltv′
F ⊢_{e} e ⇒ e′ F ⊢_{v} v ⇒ v′

F ⊢_{e} open v as ⟨t, x⟩ ine ⇒ open (get v′) as ⟨t, x⟩ ine′

F ⊢_{e} e ⇒ e′ F ⊢_{v} v ⇒ v′
F ⊢_{e} letx = v ine ⇒ letx = v′ ine′
F ⊢_{e} e ⇒ e′ F ⊢_{v} v ⇒ v′
F ⊢_{e} letx = π_{i}v ine ⇒ letx = π_{i}(get v′) ine′

\begin{matrix}F ⊢_{e} e ⇒ e′ & ℓ = F (f) \\ F ⊢_{f} f = λ(x:τ).e ⇒ λ[][r](x:M_{r}(τ)).ifgc r (gc[τ][r](cd.ℓ, x)) e′ \end{matrix}

F = {f_{i} ↦ ℓ_{1}, …} F ⊢_{f} f_{i} = λ(x:τ).e ⇒ f′_{i} F ⊢_{e} e ⇒ e′
⊢_{p} letrec \overrightarrow{f = λ(x:τ).e} ine ⇒ (\{cd ↦ \{ℓ_{1} ↦ f′_{1}, …\}\}, letregion r ine′)

Figure 3: Translation of λ_{CLOS} terms.

functions are placed into the cd region when translating code from λ_{CLOS} and never directly appear in λ_{GC} code.

5. Translating λ_{CLOS} to λ_{GC}

The translation of terms from λ_{CLOS} to λ_{GC} shown in figure 3 is mostly directed by the type translation M_{ρ} presented earlier: each function takes the current region as an argument and begins by checking if a garbage collection is necessary. All operations on data are slightly rewritten to account for the need to allocate them in the region or to fetch them from the region. For example a λ_{CLOS} function like:

fixswap(x:int× int). letx1 = π_{1}x inletx2 = π_{2}x inletx′ = (x2, x1) inhalt0

would turn into the following λ_{GC} function (apart from some synfixgc[t:Ω][r_{1}](f:∀[][r](M_{r}(t)) → 0, x:M_{r_{1}}(t)).

letregion r_{2} in lety = copy[t][r_{1}, r_{2}](x) in only {r_{2}} inf[][r_{2}](y)

fixcopy[t:Ω][r_{1}, r_{2}](x:M_{r_{1}}(t)) : M_{r_{2}}(t).

typecase t of

int ⇒ x
λ ⇒ x

t_{1} × t_{2} ⇒ letx_{1} = copy[t_{1}][r_{1}, r_{2}](π_{1}(get x)) in letx_{2} = copy[t_{2}][r_{1}, r_{2}](π_{2}(get x)) in put[r_{2}](x_{1}, x_{2})

∃t_{e} ⇒ open (get x) as ⟨t, y⟩ in letz = copy[t_{e}t][r_{1}, r_{2}](y) in put[r_{2}]⟨t=t, z:M_{r_{2}}(t_{e}t)⟩

Figure 4: The garbage collector proper.

tactic conveniences):

fixswap[][r](x:(Int× Int) atr).

ifgc r (gc[Int× Int][r](swap, x)) letx = get x in letx1 = π_{1}x in letx2 = π_{2}x in letx′ = put[r](x2, x1) in halt0

An important detail here is that the garbage collector receives the tag τ rather than the type σ of the argument. The garbage collector receives the tags for analysis as they were in λ_{CLOS} rather than as they are translated in λ_{GC}. This maintains a clear distinction between the types the programmer thinks he manipulates and the real types they map to.

Another interesting detail is that if the region is full, the function calls the garbage collector with itself as the return function. I.e. when the collection is finished, the collector will jump back to the function which will then redo the check. We could instead call the garbage collector with another function as argument. That would save us from redoing the ifgc but would require many tiny functions which are just not worth bothering with.

The translation in figure 3 uses λ_{GC} in a somewhat loose way to keep the presentation concise. More specifically, it will generate terms such as let x = π_{i}(get v) in e instead of let x′ = get v in let x = π_{i}x′ in e. Turning such code back into the strict λ_{GC} is immediate.

On the other hand, the garbage collection code in figure 4 uses not only some syntactic sugar but even resorts to using a directstyle presentation of the copy function. This is only for clarity of presentation, of course. As can be seen in figure 12 in the appendix, the code after CPS and closure conversion is a lot more difficult to read, partly because of the need to do a form of typed closure conversion [10].

The garbage collector itself is very simple: it first allocates the to region, asks copy to move everything into it and then free the from region before jumping to its continuation, using the new region.

The copy function is similarly straightforward, recursing over the whole heap and copying in a depth-first way. Clearly, the direct style here hides the stack. When the code is CPS converted and closed (as shown in the appendix), we have to allocate that stack of continuations in an additional temporary region and unless our language is extended with some notion of stack, none of those continuations would be collected until the end of the whole garbage collection. The size of this temporary region can be bounded by the size of the to region since we can’t allocate more than one continuation per copied object, so it is still algorithmically efficient, although this memory overhead is a considerable shortcoming.

6. A closer look at λ_{GC}

Programs in λ_{GC} use an allocation semantics which makes the allocation of data in memory explicit. The semantics, defined in Fig. 5, maps a machine state P to a new machine state P′. A machine state is a pair (M, e) of a memory M and a term e being executed. A memory consists of a set of regions; hence, it is defined formally as a map between region names ν and regions R. A region, in turn, is a map from offsets ℓ to storable values v. Therefore, an address is given by a pair of a region and an offset ν.ℓ. We assign a type to every location allocated in a region; Υ denotes a region type. Finally, the memory type Ψ assigns a region type to every region allocated in memory.

6.1 Closure conversion and copy.

Since the source language is monomorphic, closure conversion need only rely on existentials. This simplicity is however broken by the copy function in the garbage collector itself because this function is (recursively) polymorphic. For that reason, we also need a form of translucent type, namely ∀⟦τ⃗⟧[r⃗](σ⃗) ⟶^{ρ} 0. Closure conversion of the CPS form of copy was also the only reason for introducing ⟨α:Δ=σ_{1}, v:σ_{2}⟩.

6.2 Functions and code

Since function bodies can contain references to other functions in cdbut we do not have an easy way for the garbage collector to analyze a function body to trace through those references, cd enjoys a special status. It cannot be freed and can only contain functions, no other kind of data.

An alternative would be to require all functions to be fully closed, but that would require the addition of recursive types for the environment containing pointers to all functions and passed around everywhere. It would save us from all that cd special casing, and would allow garbage collecting code, but on the other hand, it would be less realistic since it would amount to disallowing direct function calls.

6.3 The type calculus

The target language must be expressive enough to write a tracing garbage collector. Since the garbage collector needs to know the type of values at runtime, the language λ_{GC} must support the runtime analysis of types. Therefore, conceptually, types need to play a dual role in this language. As in the source language λ_{CLOS}, they are used at compile time to type-check well formed terms. However, they are also used at runtime, as tags, to be inspected by the garbage collector (and, in general, by any type analyzing function). To enforce this distinction, we split types into a tag language and a type language. The tags correspond to the runtime entity, while the types correspond to the compile time entity.

While translating from λ_{CLOS} to λ_{GC}, the tag for a value must be constructed from its type. Therefore, the tags in λ_{GC}, closely resemble the type language in the source. To support the analysis of these tags, we need to add tag level functions (λt.τ) and tag level applications (ττ_{1}). In turn, this requires a kind calculus to classify the tags.

Types are used to classify terms. The type language includes the existential type for typing closures and the code type ∀[t⃗][r⃗](σ⃗) →

(M, ν.ℓ[τ⃗][ρ⃗](v⃗))  ⟹ (M, ν.ℓ[τ′][ρ⃗](v⃗))
\begin{matrix}(M, ν.ℓ[τ′][ρ⃗](v⃗)) \\ where M(ν.ℓ) = (λ[t⃗:κ][r⃗](x⃗:σ⃗).e) \end{matrix}  ⟹ (M, e[ρ⃗, τ′, v⃗/r⃗, t⃗, x⃗])
(M, (v⟦τ⃗⟧)[τ⃗][ρ⃗](v⃗))  ⟹ (M, v[τ⃗][ρ⃗](v⃗))
(M, letx = v ine)  ⟹ (M, e[v/x])
(M, letx = π_{i}(v_{1}, v_{2}) ine)  ⟹ (M, e[v_{i}/x])
(M, letx = put[ν]v ine)  ⟹ (M{ν.ℓ ↦ v}, e[ν.ℓ/x]) where ℓ ∉ Dom(M(ν))
(M, letx = get ν.ℓ ine)  ⟹ (M, e[v/x]) where M(ν.ℓ) = v
(M, open ⟨t=τ, v:σ⟩ as ⟨t, x⟩ ine)  ⟹ (M, open ⟨t=τ′, v:σ⟩ as ⟨t, x⟩ ine)
(M, open ⟨t=τ′, v:σ⟩ as ⟨t, x⟩ ine)  ⟹ (M, e[τ′, v/t, x])
(M, open ⟨α:Δ=σ_{1}, v:σ_{2}⟩ as ⟨α, x⟩ ine)  ⟹ (M, e[σ_{1}, v/α, x])
(M, ifgc ρ e_{1} e_{2})  ⟹ (M, e_{1}) if ρ is full
(M, ifgc ρ e_{1} e_{2})  ⟹ (M, e_{2}) if ρ is not full
(M, letregion r ine)  ⟹ (M{ν ↦ {}}, e[ν/r]) where ν ∉ Dom(M)
(M, only Δ ine)  ⟹ (M|_{Δ}, e)
(M, typecase τ of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃}))  ⟹ (M, typecase τ′ of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃}))
(M, typecase Intof (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃}))  ⟹ (M, e_{i})
(M, typecase τ → 0 of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃})) ⟹ (M, e_{λ})
(M, typecase τ_{1} × τ_{2} of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃})) ⟹ (M, e_{×}[τ_{1}, τ_{2}/t_{1}, t_{2}])
(M, typecase ∃t.τ of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃})) ⟹ (M, e_{∃}[λt.τ/t_{e}])

Figure 5: Operational semantics of λ_{GC}.

0 for fully closed functions. Moreover, types in the target language must include the region in which the corresponding value resides. Therefore, we use the notation σ atρ for the type of a value of type σ in region ρ.

To reason about the safety of programs in this language, we will often need to assume that a value resides in a particular region only. For example, after the copy function is finished, we must be able to assume that all the data is contained only in the new region; so that the old region can be safely freed. Therefore, to ensure type safety, we must be able to enforce this invariant at the type level. For this, we use the built in type operator M. The type M_{ρ}(τ) can only contain values that are in region ρ. Notice that it is a restricted form of the fully reflexive Typerec operator [19]. Essentially, it is a Typerec that has been hard-wired into the language.

6.4 The term calculus

The term language must support region based memory management and runtime type analysis. New regions are created through the let region r in e construct which allocates a new region ν at runtime and binds r to it. A term of the form put[ρ]v allocates a value v in the region ρ. Data is read from a region in two ways. Functions are read implicitly through a function call. Data may also be read through the get v construct. Operationally, the get construct takes a memory address ν.ℓ and dereferences it.

Deallocation is handled implicitly through the only Δ in e construct [21]. It asserts statically that the expression e can be evaluated using the set of regions bound to Δ′ and the code region, which is a subset of the region variables currently in scope.

Ψ|_{Δ′}; Δ′, cd; Θ; Φ|_{Δ′}; Γ|_{Δ′} ⊢ e Δ′ ⊂ Δ

Ψ; Δ; Θ; Φ; Γ ⊢ only Δ′ ine

The memory is restricted to the set of regions in Δ′ (Ψ|_{Δ′}) and the code region. Similarly, the other environments (Φ and Γ) are restricted to be well formed under Δ′ (Φ|_{Δ′} and Γ|_{Δ′}). At runtime, an implementation would treat the set of regions in Δ′ as live and reclaim other regions. Since the reclamation works on whole regions, the cost is proportional to the number of regions. Since this number is usually small, it entails an insignificant runtime penalty. The dynamic check takes care of aliasing. This makes our system significantly simpler since we can avoid the heavy type machinery required to detect aliasing statically.

The runtime type analysis is handled through a typecase construct. Depending on the head of the type being analyzed, the typecase chooses one of the branches for execution. When analyzing a type variable t, we refine types containing t in each of the branches [6].

Θ ⊢ t : Ω
Ψ; Δ; Θ; Φ; Γ[int/t] ⊢ e_{i}[int/t]
…
Ψ; Δ; Θ; Φ; Γ ⊢ typecase t of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃})

In the e_{i} branch, we know that the type variable t is bound to Int and can therefore substitute it away. A similar rule is applied to the other cases.

6.5 Formal properties of the language

In this section, we prove that type checking in λ_{GC} is decidable and that the calculus is sound. We omit the proofs due to space constraints. The reader may refer to the companion technical report for details.

6.5.1 Type checking is decidable

Proposition 6.1 Reduction of well formed types is strongly nor-

[figure: Θ ⊢ τ : κ]

· ⊢ Int: Ω {Θ(t) = κ \atop Θ ⊢ t : κ} {Θ ⊢ τ_{1} : Ω Θ ⊢ τ_{2} : Ω \atop Θ ⊢ τ_{1} × τ_{2} : Ω}

{Θ ⊢ τ_{i} : Ω \atop Θ ⊢ τ⃗ → 0 : Ω}  {Θ, t:Ω ⊢ τ : Ω \atop Θ ⊢ ∃t.τ : Ω}

{Θ, t:Ω ⊢ τ : Ω \atop Θ ⊢ λt.τ : Ω ⟶ Ω} {Θ ⊢ τ_{1} : Ω ⟶ Ω  Θ ⊢ τ_{2} : Ω \atop Θ ⊢ τ_{1}τ_{2} : Ω}

[figure: Δ; Θ; Φ ⊢ σ]

Δ; Θ; Φ ⊢ int Δ; Θ; Φ ⊢ σ_{1} Δ; Θ; Φ ⊢ σ_{2}

Δ; Θ; Φ ⊢ σ_{1} × σ_{2}

{\{r⃗\}; t⃗:κ; · ⊢ σ_{i} \atop Δ; Θ; Φ ⊢ ∀[t⃗:κ][r⃗](σ⃗) → 0}  {Δ; Θ, t:κ; Φ ⊢ σ \atop Δ; Θ; Φ ⊢ ∃t:κ.σ}

Δ; Θ; Φ ⊢ σ ρ ∈ Δ Δ; Θ; Φ ⊢ σ atρ

{Θ ⊢ τ : Ω ρ ∈ Δ \atop Δ; Θ; Φ ⊢ M_{ρ}(τ)}

\begin{matrix}Φ(α) = Δ′ & Δ′ ⊂ Δ \\ Δ; Θ; Φ ⊢ α \end{matrix} Δ; Θ; Φ, α:Δ′ ⊢ σ Δ′ ⊂ Δ

Δ; Θ; Φ ⊢ ∃α:Δ′.σ

{\{r⃗\}; Θ; · ⊢ σ_{i} Θ ⊢ τ_{i} : κ_{i} ρ ∈ Δ \atop Δ; Θ; Φ ⊢ ∀⟦τ⃗⟧[r⃗](σ⃗) ⟶^{ρ} 0}

[figure]

Ψ; Δ; Θ; Φ; Γ ⊢ v : σ Ψ; Δ; Θ; Φ; Γ ⊢ op : σ

Ψ; Δ; Θ; Φ; Γ ⊢ n : int {Γ(x) = σ \atop Ψ; Δ; Θ; Φ; Γ ⊢ x : σ}
Ψ(ν.ℓ) = σ Dom(Ψ); ·; · ⊢ σ atν

Ψ; Δ; Θ; Φ; Γ ⊢ ν.ℓ : σ atν

cd, r⃗; t⃗; · ⊢ σ_{i} Ψ|cd; cd, r⃗; \overrightarrow{t:κ}; ·; \overrightarrow{x:σ} ⊢ e Ψ; Δ; Θ; Φ; Γ ⊢ λ[t⃗:κ][r⃗](\overrightarrow{x:σ}).e : ∀[t⃗:κ][r⃗](σ⃗) → 0

Ψ; Δ; Θ; Φ; Γ ⊢ v : ∀[t⃗:κ][r⃗](σ⃗) → 0 atρ Θ ⊢ τ_{i} : κ_{i}

Ψ; Δ; Θ; Φ; Γ ⊢ v⟦τ⃗⟧ : ∀⟦τ⃗⟧[r⃗](σ⃗[τ⃗/t⃗]) ⟶^{ρ} 0

Ψ; Δ; Θ; Φ; Γ ⊢ v_{1} : σ_{1} Ψ; Δ; Θ; Φ; Γ ⊢ v_{2} : σ_{2} Ψ; Δ; Θ; Φ; Γ ⊢ (v_{1}, v_{2}) : σ_{1} × σ_{2}

Ψ; Δ; Θ; Φ; Γ ⊢ v : σ_{1} × σ_{2} Ψ; Δ; Θ; Φ; Γ ⊢ π_{i}v : σ_{i} Ψ; Δ; Θ; Φ; Γ ⊢ v : σ atρ Ψ; Δ; Θ; Φ; Γ ⊢ get v : σ

Θ ⊢ τ : κ Ψ; Δ; Θ; Φ; Γ ⊢ v : σ[τ/t]

Ψ; Δ; Θ; Φ; Γ ⊢ ⟨t=τ, v:σ⟩ : ∃t:κ.σ

Δ′; Θ; Φ|_{Δ′} ⊢ σ_{1} Ψ; Δ; Θ; Φ; Γ ⊢ v : σ_{2}[σ_{1}/α]

Ψ; Δ; Θ; Φ; Γ ⊢ ⟨α:Δ′ =σ_{1}, v:σ_{2}⟩ : ∃α:Δ′.σ_{2}

Ψ; Δ; Θ; Φ; Γ ⊢ v : σ ρ ∈ Δ Ψ; Δ; Θ; Φ; Γ ⊢ put[ρ]v : σ atρ

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

Ψ; Δ; Θ; Φ; Γ ⊢ v : ∀[t⃗:κ][r⃗](σ⃗) → 0 atρ

Ψ; Δ; Θ; Φ; Γ ⊢ v_{i} : σ_{i}[ρ⃗, τ⃗/r⃗, t⃗] Θ ⊢ τ_{i} : κ_{i} ρ_{i} ∈ Δ Ψ; Δ; Θ; Φ; Γ ⊢ v[τ⃗][ρ⃗](v⃗)

Ψ; Δ; Θ; Φ; Γ ⊢ v : ∀⟦τ⃗⟧[r⃗](σ⃗) ⟶^{ρ} 0

Ψ; Δ; Θ; Φ; Γ ⊢ v_{i} : σ_{i}[ρ⃗/r⃗] ρ_{i} ∈ Δ

Ψ; Δ; Θ; Φ; Γ ⊢ v[τ⃗][ρ⃗](v⃗)

Ψ; Δ; Θ; Φ; Γ ⊢ op : σ Ψ; Δ; Θ; Φ; Γ, x:σ ⊢ e Ψ; Δ; Θ; Φ; Γ ⊢ letx = op ine

Ψ; Δ; Θ; Φ; Γ ⊢ v : ∃t′:κ.σ Ψ; Δ; Θ, t:κ; Φ; Γ, x:σ[t/t′] ⊢ e Ψ; Δ; Θ; Φ; Γ ⊢ open v as ⟨t, x⟩ ine

Ψ; Δ; Θ; Φ; Γ ⊢ v : ∃α′:Δ′.σ Ψ; Δ; Θ; Φ, α:Δ′; Γ, x:σ[α/α′] ⊢ e Ψ; Δ; Θ; Φ; Γ ⊢ open v as ⟨α, x⟩ ine

Ψ; Δ; Θ; Φ; Γ ⊢ e_{1} Ψ; Δ; Θ; Φ; Γ ⊢ e_{2} ρ ∈ Δ Ψ; Δ; Θ; Φ; Γ ⊢ ifgc ρ e_{1} e_{2}

Ψ; Δ, r; Θ; Φ; Γ ⊢ e Ψ; Δ; Θ; Φ; Γ ⊢ letregion r ine Ψ; Δ; Θ; Φ; Γ ⊢ v : int Ψ; Δ; Θ; Φ; Γ ⊢ haltv

Ψ|_{Δ′}; Δ′, cd; Θ; Φ|_{Δ′}; Γ|_{Δ′} ⊢ e Δ′ ⊂ Δ

Ψ; Δ; Θ; Φ; Γ ⊢ only Δ′ ine

Ψ; Δ; Θ; Φ; Γ ⊢ ei

Ψ; Δ; Θ; Φ; Γ ⊢ typecase Intof (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃})

Ψ; Δ; Θ; Φ; Γ ⊢ e_{λ}

Ψ; Δ; Θ; Φ; Γ ⊢ typecase τ⃗ → 0 of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃})

Ψ; Δ; Θ; Φ; Γ ⊢ e_{×}[τ_{1}, τ_{2}/t_{1}, t_{2}]

Ψ; Δ; Θ; Φ; Γ ⊢ typecase (τ_{1} × τ_{2}) of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃})

Ψ; Δ; Θ; Φ; Γ ⊢ e_{∃}[λt.τ/t_{e}]

Ψ; Δ; Θ; Φ; Γ ⊢ typecase ∃t.τ of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃})

Θ ⊢ t : Ω Ψ; Δ; Θ; Φ; Γ[int/t] ⊢ e_{i}[int/t] Ψ; Δ; Θ; Φ; Γ ⊢ e_{λ} Ψ; Δ; Θ, t_{1} :Ω, t_{2} :Ω; Φ; Γ[t_{1} × t_{2}/t] ⊢ e_{×}[t_{1} × t_{2}/t] Ψ; Δ; Θ, t_{e}:Ω ⟶ Ω; Φ; Γ[∃t.t_{e}t/t] ⊢ e_{∃}[∃t.t_{e}t/t] Ψ; Δ; Θ; Φ; Γ ⊢ typecase t of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃})

Figure 6: Static semantics of λ_{GC}.

[figure: Δ ⊢ Υ ⊢ Ψ]

{Δ; ·; · ⊢ σ_{i} \atop Δ ⊢ \{ℓ_{1} :σ_{1}, …, ℓ_{n}:σ_{n}\}}  {\{ν_{1}, …, ν_{n}\} ⊢ Υ_{i} \atop ⊢ \{ν_{1} :Υ_{1}, …, ν_{n}:Υ_{n}\}}

Υcd = \{ℓ_{1} :∀[τ⃗_{1}][r⃗_{1}](\overrightarrow{v_{1} :σ_{1}}) → 0, …, ℓ_{n}:∀[τ⃗_{n}][r⃗_{n}](\overrightarrow{v_{n}:σ_{n}}) → 0\}

[figure: Ψ ⊢ R : Υ ⊢ M : Ψ]

{Ψ; Dom(Ψ); ·; ·; · ⊢ v_{i} : σ_{i} \atop Ψ ⊢ \{ℓ_{1} ↦ v_{1}, …, ℓ_{n} ↦ v_{n}\} : \{ℓ_{1} :σ_{1}, …, ℓ_{n}:σ_{n}\}}

{⊢ \{ν_{1} :Υ_{1}, …, ν_{n}:Υ_{n}\} \{ν_{1} :Υ_{1}, …, ν_{n}:Υ_{n}\} ⊢ R_{i} : Υ_{i} \atop ⊢ \{ν_{1} ↦ R_{1}, …, ν_{n} ↦ R_{n}\} : \{ν_{1} :Υ_{1}, …, ν_{n}:Υ_{n}\}}

Figure 7: Environment formation rules.

malizing.

Proof Since the tag language is a simply typed lambda calculus, reduction of well formed tags is strongly normalizing and confluent. The termination of M_{ρ}(τ) follows from a straightforward induction on the size of the tag τ.

Proposition 6.2 Reduction of well formed types is confluent.

Proof Since the reduction of well formed types is strongly normalizing, confluence of the reduction follows from local confluence. This follows easily from a case analysis of the reduction of the M_{ρ}(τ) tag.

6.5.2 Soundness

Definition 6.3 The machine state (M, e) is well formed iff

{⊢ M:Ψ Ψ; Dom(Ψ); ·; ·; · ⊢ e \atop ⊢ (M, e)}

Contrary to the other environments, Ψ is not explicitly constructed in any of the static rules, since it reflects dynamic information. Instead, the soundness proof, or more specifically the type preservation proof, needs to construct some witness Ψ′ for the new state (M′, e′) based on the Ψ of the initial state (M, e).

Proposition 6.4 (Type Preservation) If ⊢ (M, e) and (M, e) ⟹ (M′, e′) then ⊢ (M′, e′). Proof See the appendix A.

Proposition 6.5 (Progress) If ⊢ (M, e) then either e = haltv or there exists a (M′, e′) such that (M, e) ⟹ (M′, e′). Proof See the appendix A.

7. Forwarding pointers

The base algorithm presented before is unrealistic in a number of ways. The first is the fact that the copy function does not preserve sharing and thus turns any DAG into a tree.

We hence need to add some form of forwarding pointers. Wang and Appel suggest to pair up every object with its forwarding pointer,

[figure]

Ψ; Δ; Θ; Φ; Γ ⊢ v : σ Ψ; Δ; Θ; Φ; Γ ⊢ e

Ψ; Δ; Θ; Φ; Γ ⊢ v : leftσ Ψ; Δ; Θ; Φ; Γ ⊢ stripv : σ Ψ; Δ; Θ; Φ; Γ ⊢ v : rightσ Ψ; Δ; Θ; Φ; Γ ⊢ stripv : σ

Ψ; Δ; Θ; Φ; Γ ⊢ v : σ Ψ; Δ; Θ; Φ; Γ ⊢ inlv : leftσ

Ψ; Δ; Θ; Φ; Γ ⊢ v : σ

Ψ; Δ; Θ; Φ; Γ ⊢ inrv : rightσ

Ψ; Δ; Θ; Φ; Γ ⊢ v : σ_{1}
Ψ; Δ; Θ; Φ; Γ ⊢ v : σ_{1} + σ_{2}

Ψ; Δ; Θ; Φ; Γ ⊢ v : σ_{2} Ψ; Δ; Θ; Φ; Γ ⊢ v : σ_{1} + σ_{2}

Ψ; Δ; Θ; Φ; Γ ⊢ v : σ_{1} + σ_{2}

Ψ; Δ; Θ; Φ; Γ, x:σ_{1} ⊢ e_{l} Ψ; Δ; Θ; Φ; Γ, x:σ_{2} ⊢ e_{r}

Ψ; Δ; Θ; Φ; Γ ⊢ ifleftx = v e_{l} e_{r}
Ψ; Δ; Θ; Φ; Γ ⊢ e

Ψ; Δ; Θ; Φ; Γ ⊢ v_{1} : σ atρ Ψ; Δ; Θ; Φ; Γ ⊢ v_{2} : σ

Ψ; Δ; Θ; Φ; Γ ⊢ set v_{1} := v_{2} ; e
Ψ; Δ; Θ; Φ; Γ ⊢ v : M_{ρ}(τ)

Ψ|cd; cd, ρ, ρ′; Θ; Φ|_{ρρ′}; x:C_{ρ,ρ′}(τ) ⊢ e

Ψ; Δ; Θ; Φ; Γ ⊢ letx = widen[ρ′][τ](v) ine

Figure 8: Static semantics for λ_{GCforw}.

incurring a significant memory cost.^{1} We want instead to represent objects as a sum (σ + fwdσ), which requires a single bit per object and corresponds much more closely to traditional implementations. To this end, λ_{GCforw} extends λ_{GC} with new types and terms for tag bits and sum types as well as memory assignment. We do not need a new fwd or ref type since we can use the region calculus’ references for that purpose.

Another requirement for a realistic GC is that the mutator should not need to constantly check for the presence of forwarding pointers since such a read-barrier would only be justified for an incremental GC. In other words, the type as seen by the mutator should not be a sum, although it should still contain the single-bit tag that the GC will use to distinguish between forwarding pointers. Also there should be a way to switch from the mutator’s view of the type of an object to the one of the collector. So we also need to add a form of cast that we call widen which we will use at the beginning of a collection to give the collector access to the forwarding pointers:

σ ::= … | leftσ | rightσ | leftσ_{1} + rightσ_{2} | C_{ρ,ρ′}(τ)
v ::= … | inlv | inrv
op ::= … | stripv
e ::= … | ifleftx = v e_{l} e_{r} | set v_{1} := v_{2} ; e | letx = widen[ρ][τ](v) ine

inl and inr(and their type-level counterparts left and right) can be thought of as adding a single tag bit to an object while strip gets back the untagged object and ifleft checks the tag bit. The idea is to represent objects as (left σ) to the mutator (without the (rightσ) alternative to avoid the need for checks) and cast them with the widen operator to (leftσ + right(σ atto)) when entering

1This additional word is not unheard of, since replicating garbage collectors [14, 1] incur a similar overhead, justified by the desire to provide concurrent collection while avoiding the cost of a readbarrier. the garbage collector (here “to” denotes the region variable for the to space).

Since a single source-level type now maps to two different possible types, we need two type operators: M_{ρ}(τ) to map source types to the mutator’s view of the data and C_{ρ,ρ′}(τ) to map source types to the collector’s view (which adds forwarding pointers). M_{ρ}(τ) is the same as before for base types and for code types, but is changed for existentials and pairs by adding the left constructor that constrains the mutator to provide the tag bit needed to distinguish the forwarded pointer from the non-forwarded data.

M_{ρ}(Int)  ⟹ int
M_{ρ}(τ → 0) ⟹ ∀[][r](M_{r}(τ)) → 0 atcd
M_{ρ}(∃t.τ)  ⟹ (left(∃t.M_{ρ}(τ))) atρ
M_{ρ}(τ_{1} × τ_{2}) ⟹ (left(M_{ρ}(τ_{1}) × M_{ρ}(τ_{2}))) atρ
C_{ρ,ρ′}(Int)  ⟹ int
C_{ρ,ρ′}(τ → 0) ⟹ M_{ρ}(τ → 0)
C_{ρ,ρ′}(∃t.τ) ⟹ (left(∃t.C_{ρ,ρ′}(τ)) + right(M_{ρ′}(∃t.τ))) atρ
C_{ρ,ρ′}(τ_{1} × τ_{2}) ⟹ (+\begin{matrix}left(C_{ρ,ρ′}(τ_{1}) × C_{ρ,ρ′}(τ_{2})) \\ right(M_{ρ′}(τ_{1} × τ_{2})) \end{matrix}) atρ

It is worth noting again here how the M type operators cleanly encapsulate the invariants imposed on the mutator by the collector. In this case, it forces the mutator to provide the collector with free bit that the collector can then use to distinguish forwarding pointers from non-forwarded data. And we also see how the same mechanism can be used to express the difference between the restricted view offered to the mutator and the full blown access to internal data that the collector needs.

The operational semantics of the new operations is straightforward, especially since we can implement the assignment operator by reusing the indirection through the memory:

(M, letx = strip(inlv) ine) ⟹ (M, e[v/x])
(M, letx = strip(inrv) ine) ⟹ (M, e[v/x])
(M, ifleftx = (inlv) e_{l} e_{r})  ⟹ (M, e_{l}[inlv/x])
(M, ifleftx = (inrv) e_{l} e_{r})  ⟹ (M, e_{l}[inrv/x])
(M, set ν.ℓ := v ; e)  ⟹ (M{ν.ℓ ↦ v}, e)
(M, letx = widen[ρ][τ](v) ine) ⟹ (M, e[v/x])

The translation from λ_{CLOS} to this λ_{GCforw} is not shown since it is basically the same as before except for the insertion of all the inl and strip. The garbage collector can be seen in figure 9. Compared to the original algorithm, the only difference in the gc function itself is the widening of the heap from M_{r1} to C_{r1,r2} and the fact that we have to bundle the f and x arguments into a pair in order to pass it through the widen operator and unbundle it afterwards. The copy function also needed to be changed of course: when copying a heap object such as a pair, it now has to check with ifleftwhether the object was forwarded, if so it just returns the forwarded object, otherwise it does the copy as before and has to overwrite (using set) the original object with the forwarding pointer before returning the copied object.

7.1 How to widen safely

The only non-trivial extension is widen which allows the garbage collector to have a different view of the existing memory, provided the two views are somehow compatible. It seems difficult to solve the problem of allowing two views on the same data without such a form of cast. At first, it seems we are just applying a form of subtyping, but this form of subtyping is very powerful since it allows fixgc[t:Ω][r_{1}](f:M_{r_{1}}(λ(t)), x:M_{r_{1}}(t)).

letregion r_{2} in

letw = widen[r_{2}][(λ(t) × t)](put[r_{1}](inl(f, x))) in ifleftw = get w then letw = stripw in lety = copy[t][r_{1}, r_{2}](π_{2}w) in only {r_{2}} in(π_{1}w)[][r_{2}](y)

else halt0

fixcopy[t:Ω][r_{1}, r_{2}](x:C_{r_{1},r_{2}}(t)) : M_{r_{2}}(t).

typecase t of

int ⇒ x
λ ⇒ x

t_{1} × t_{2} ⇒ lety = get x in

iflefty = y then letx_{1} = copy[t_{1}][r_{1}, r_{2}](π_{1}(stripy)) in letx_{2} = copy[t_{2}][r_{1}, r_{2}](π_{2}(stripy)) in letz = put[r_{2}](inl(x_{1}, x_{2})) in set x := inrz ; z

else

stripy

∃t_{e} ⇒ lety = get x in

iflefty = y then open (stripy) as ⟨t, y⟩ in lety = copy[t_{e}t][r_{1}, r_{2}](y) in letz = put[r_{2}](inl⟨t=t, y:M_{r_{2}}(t_{e}t)⟩) in set x := inrz ; z

else stripy

Figure 9: GC with forwarding pointers.

covariant subtyping of references. This means that aliasing issues have to be handled with extreme care.

When faced with the same problem, Wang and Appel came up independently with a similar idea. But their suggested cast leaves many questions open and might need more work to be made typesafe. Also its operational semantics actually does a complete copy of the heap from one region to the other. This might make it easier to prove soundness but makes it unclear whether it can really be implemented as a nop. In contrast, the operational semantics of widen is a nop and we have a proof of its soundness.

In order to handle the problem of aliasing mentioned above, it might be possible to rely on some form of linear typing or alias types [20], but given the inherent generality of a garbage collector, it seems difficult. Our approach is to rely on the consistent application of the same cast over the whole heap, so that aliases are guaranteed to be cast in the same way.

Rather than an ad-hoc widen we could provide a more general cast that can consistently apply iteratively some type transformations (as long as it obeys the notion of subtyping extended with covariant subtyping of references) to any particular set of regions, but the complexity of such an operator is out of the scope of this paper.

In Figure 8, the typing rule for widen shows that the expression e is typed in an environment that only contains x. In essence x represents the entire heap. Further, x is obtained from the value v that has type M_{ρ}(τ). Looking at the definition of M, we can see that all values reachable from v will have a type of the form M_{ρ}(τ′). Since both Mand C are iterators, we can now define a casting operation from one type to the other as an iterator. This iterator will traverse the entire heap and systematically convert from one type to the other; this systematic conversion is necessary to avoid ending up with a value that has a particular type along one path, but has a different type along another path.

The proof of soundness of widen is rather intricate. It starts by ignoring all the dead objects from the heap, so that only objects of type M_{ρ}(τ) are left, which get cast to C_{ρ,ρ′}(τ). For that reason, we needed to loosen our notion of a well formed machine state to allow restricting the considered memory M to just a well-typed sufficient subset \overline{M}, where “sufficient” means that no object outside of \overline{M} is needed to complete execution. This safely permits ill-typed garbage.

Definition 7.1 The machine state (M, e) is well formed iff

\begin{aligned}\overline{M} ⊂ M & ⊢ \overline{M}:Ψ & Ψ; Dom(Ψ); ·; ·; · ⊢ e \\ & ⊢ (M, e) \end{aligned}

Proposition 7.2 (Type Preservation) If ⊢ (M, e) and (M, e) ⟹ (M′, e′) then ⊢ (M′, e′). Proof See the appendix C.

Proposition 7.3 (Progress) If ⊢ (M, e) then either e = haltv or there exists a (M′, e′) such that (M, e) ⟹ (M′, e′). Proof See the appendix C.

8. Generational collection

Another important aspect of a modern GC is the support for generational garbage collection. If we first restrict ourselves to a sideeffect free language, then we can collect a single generation at a time so long as we can express the fact that an object in the old generation cannot point to an object in the young generation.

To that end we need to extend λ_{GC} with existential quantification over regions, so that the mutator does not need to care whether an object is allocated in the young or the old region. We also need to add some way to check in which region an object is allocated so that GC can detect when an object is in the old generation (and hence does not need copying):

σ ::= … | ∃r ∈Δ.(σ atr)
v ::= … | ⟨r ∈ Δ = ρ, v:σ⟩
e ::= … | open v as ⟨r, x⟩ ine | ifreg (ρ_{1} = ρ_{2}) e_{1} e_{2}

Apart from those new constructs (whose static semantics is presented in figure 10), the Mtype operator also needs to be modified to reflect the new invariant imposed on the mutator. It is now indexed by two regions (the old and the new) and has to enforce the fact that objects in the old region cannot have references to the new region:

M_{ρ_{y},ρ_{o}}(Int)  ⟹ int
M_{ρ_{y},ρ_{o}}(τ → 0) ⟹ ∀[][r_{y}, r_{o}](M_{r_{y},r_{o}}(τ)) → 0 atcd
M_{ρ_{y},ρ_{o}}(∃t.τ) ⟹ ∃r ∈{ρ_{y}, ρ_{o}}.((∃t.M_{r,ρ_{o}}(τ)) atr)
M_{ρ_{y},ρ_{o}}(τ_{1} × τ_{2}) ⟹ ∃r ∈{ρ_{y}, ρ_{o}}.((M_{r,ρ_{o}}(τ_{1}) × M_{r,ρ_{o}}(τ_{2})) atr)

By using the set {r, ρ_{o}} we make sure that if r is the old generation, pointers underneath it cannot point back to the new generation.

The operational semantics are again rather simple:

(M, open ⟨r ∈ Δ = ν, v:σ⟩ as ⟨r, x⟩ ine) ⟹ (M, e[ν, v/r, x])
(M, ifreg (ν = ν) e_{1} e_{2})  ⟹ (M, e_{1})
(M, ifreg (ν_{1} = ν_{2}) e_{1} e_{2})  ⟹ (M, e_{2})

[figure]

Δ; Θ; Φ ⊢ σ  Ψ; Δ; Θ; Φ; Γ ⊢ v : σ  Ψ; Δ; Θ; Φ; Γ ⊢ e
Δ′ ⊂ Δ Δ, r; Θ; Φ ⊢ σ
Δ; Θ; Φ ⊢ ∃r ∈Δ′.(σ atr)

Θ ⊢ τ : Ω ρ_{1} ∈ Δ ρ_{2} ∈ Δ
Δ; Θ; Φ ⊢ M_{ρ_{1},ρ_{2}}(τ)

Ψ; Δ; Θ; Φ; Γ ⊢ v : σ[ρ/r] atρ ρ ∈ Δ′ Δ′ ⊂ Δ
Ψ; Δ; Θ; Φ; Γ ⊢ ⟨r ∈ Δ′ = ρ, v:σ⟩ : ∃r ∈Δ′.(σ atr)

Ψ; Δ; Θ; Φ; Γ ⊢ v : ∃r ∈Δ′.(σ atr)

Ψ; Δ, r; Θ; Φ; Γ, x:σ atr ⊢ e

Ψ; Δ; Θ; Φ; Γ ⊢ open v as ⟨r, x⟩ ine

Ψ; Δ[r, r/r_{1}, r_{2}]; Θ; Φ[r, r/r_{1}, r_{2}]; Γ[r, r/r_{1}, r_{2}] ⊢ e_{1}[r, r/r_{1}, r_{2}]
Ψ; Δ; Θ; Φ; Γ ⊢ e_{2} r ∉ Δ

Ψ; Δ; Θ; Φ; Γ ⊢ ifreg (r_{1} = r_{2}) e_{1} e_{2}

Ψ; Δ[ν/r]; Θ; Φ[ν/r]; Γ[ν/r] ⊢ e_{1}[ν/r] Ψ; Δ; Θ; Φ; Γ ⊢ e_{2}

Ψ; Δ; Θ; Φ; Γ ⊢ ifreg (r = ν) e_{1} e_{2} Ψ; Δ; Θ; Φ; Γ ⊢ ifreg (ν = r) e_{1} e_{2}

Ψ; Δ; Θ; Φ; Γ ⊢ e_{2}

Ψ; Δ; Θ; Φ; Γ ⊢ ifreg (ν_{1} = ν_{2}) e_{1} e_{2}

Ψ; Δ; Θ; Φ; Γ ⊢ e_{1}

Ψ; Δ; Θ; Φ; Γ ⊢ ifreg (ν_{1} = ν_{1}) e_{1} e_{2}

Figure 10: Static semantics of λ_{GCgen}.

Although the operational semantics do not take advantage of it (in order to simplify the soundness proof), we defined the existentials over regions in such a way that they can be implemented as nop since the encapsulated reference usually already encodes the region in its bit-pattern (or in its ν.ℓ).

The new term translation is again not shown since it is so similar to the original one. The new type constraint is trivially always satisfied as long as the mutator only allocates from the younger generation and as long as the memory is immutable. If side-effects were to be necessary, it should be possible to extend this scheme with one mutable region (keeping all others immutable) which would be considered similarly to the older generation but scanned at each collection. Obviously, this would first require adding some way to scan a region, but should not present any serious difficulty.

The GC itself can be seen in figure 11. The main difference with the basic GC of figure 4 is that it does not copy to a new region but to an existing one and stops traversing the tree as soon as we encounter a reference to the old generation.

When hitting such an external reference, we have to repack it just to help the type-system understand that this reference is of type M_{ρ_{y},ρ_{o}}(τ). But those operations are free anyway.

Note that another function needs to be written to garbage collect the old generation, but that one is the same as the non-generational one.

At first sight, the λ_{GCgen} language may seem unsound because we allow existentials over regions. However, these types are not existentials in a real sense since they do not hide a region within a type. Rather, in the type ∃r ∈ Δ.(σ at r), the set Δ is an upper bound on the regions that the variable r may range over. In this fixgc[t:Ω][r_{y}, r_{o}](f:M_{r_{y},r_{o}}(∀[][](t) → 0), x:M_{r_{y},r_{o}}(t)).

lety = copy[t][r_{y}, r_{o}](x) in

only {r_{o}} inletregion r_{y} inf[][r_{y}, r_{o}](y)

fixcopy[t:Ω][r_{y}, r_{o}](x:M_{r_{y},r_{o}}(t)) : M_{r_{o},r_{o}}(t).

typecase t of

int ⇒ x
λ ⇒ x

t_{1} × t_{2} ⇒ open x as ⟨r, x⟩ in

ifreg r = r_{o} then ⟨r ∈ {r_{o}} = r_{o}, x⟩ else letx_{1} = copy[t_{1}][r_{y}, r_{o}](π_{1}(get x)) in letx_{2} = copy[t_{2}][r_{y}, r_{o}](π_{2}(get x)) in ⟨r ∈ {r_{o}} = r_{o}, put[r](x_{1}, x_{2})⟩

∃t_{e} ⇒ open x as ⟨r, x⟩ in

ifreg r = r_{o} then ⟨r ∈ {r_{o}} = r_{o}, x⟩ else open (get x) as ⟨t, y⟩ in letz = copy[t_{e}t][r_{y}, r_{o}](y) in ⟨r ∈ {r_{o}} = r_{o}, put[r]⟨t=t, z:M_{r,r_{o}}(t_{e}t)⟩⟩

Figure 11: Generational GC.

sense, our existential is closer to a bounded quantification.

Proposition 8.1 (Type Preservation) If ⊢ (M, e) and (M, e) ⟹ (M′, e′) then ⊢ (M′, e′). Proof See the appendix D.

Proposition 8.2 (Progress) If ⊢ (M, e) then either e = haltv or there exists a (M′, e′) such that (M, e) ⟹ (M′, e′). Proof See the appendix D.

9. Related work

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. The main weakness of their proposal is that it relies on a closure conversion algorithm due to Tolmach [18] that represents closures as datatypes. This makes closures transparent, making it easier for the copy function to analyze, but it requires whole program analysis and has major drawbacks in the presence of separate compilation. We believe it is more natural to represent closures as existentials [10, 9] and we show how to use intentional type analysis (on quantified types [19]) to typecheck the GC-copy function.

The idea of intensional type analysis was first proposed by Harper and Morrisett [8]. They introduced the idea of having explicit type analysis operators which inductively traverse the structure of types. However, to retain decidability of type checking, they restrict the analysis to a predicative subset of the type language. Crary et al. [5] propose a very powerful type analysis framework. They define a rich kind calculus that includes sum kinds and inductive kinds. They also provide primitive recursion at the type level. Therefore, they can define new kinds within their calculus and directly encode type analysis operators within their language. They also include a novel refinement operation at the term level. Saha et al [19] shows how to handle polymorphic functions that analyze the quantified type variable—this allows the type analysis to handle arbitrary quantified types. The typerec operators (e.g., M_{ρ}) used in this paper do not require the full power of what is provided in [19] because our source language is only a simply typed lambda calculus.

Tofte and Talpin [17] proposed to use region calculus to type check memory management for higher-order functional languages.

Crary et al [4] presented a low-level typed intermediate language that can express explicit region allocation and deallocation. Our λ_{GC} language borrows the basic organization of memories and regions from Crary et al [4]. The main difference is that we don’t require explicit capabilities—region deallocation is handled through the only primitive.

Necula [13] proposed the idea of a certifying compiler and showed the construction of a certifying compiler for a type-safe subset of C. Morrisett et al. [12] showed that a fully type preserving compiler generating type safe assembly code is a practical basis for a certifying compiler. This paper shows that low-level runtime services such as garbage collection can also be expressed in a type safe language.

10. Conclusion and future work

We have presented a type-safe intermediate language with regions and intensional type analysis and show how it can be used to provide a simple and provably type-safe stop-and-copy tracing garbage collector. Our key idea is to use intensional type analysis on quantified types (i.e., existentials) to express the garbagecollection invariants on the mutator data objects. We show how this same idea can be used to express more realistic scavengers with efficient forwarding pointers and generations. Because intensional type analysis is also applicable to polymorphic lambda calculus [19], we believe our type safe collector can be extended to handle polymorphic languages as well.

We intend to extend our collector with the following features, which a modern garbage collector should be able to provide:

• Polymorphism. Intensional type analysis is a powerful framework. Adding support for polymorphism is straightforward but tedious because the type-system becomes a lot heavier.

• Cyclic data structures. It might be possible to extend the current depth-first copying approach to properly handle cycles, but we are more interested in a Cheney-style breadthfirst copy [2].

• Side-effects and generations. A first approach could be to extend our current generation scheme with a third region containing all the mutable data. But ultimately we will need to use either card-marking or remembered-sets [25].

• Explicit tag storage. Since tags exist at run time, we need to garbage collect them as well. The most promising approach is to reify them into special terms as was done by Crary et al [6, 5]. This will also allow us to use a simpler closure conversion algorithm for polymorphic code, eliminating the need for translucent types.

References

[1] G. Blelloch and P. Cheng. On bounding time and space for multiprocessor garbage collection. In Symposium on Programming Languages Design and Implementation, pages 104–107. ACM Press, May 1999.

[2] C. J. Cheney. A non-recursive list compacting algorithm. Commun. ACM, 13(11):677–678, 1970.

[3] K. Crary. Typed assembly language: Type theory for machine code. Talk presented at 2000 PCC Workshop, Santa Barbara, CA, June 2000.

[4] 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.

[5] K. Crary and S. Weirich. Flexible type analysis. In Proc. 1999 ACM SIGPLAN International Conference on Functional Programming, pages 233–248. ACM Press, Sept. 1999.

[6] K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In Proc. 1998 ACM SIGPLAN International Conference on Functional Programming, pages 301–312. ACM Press, Sept. 1998.

[7] O. Danvy and A. Filinski. Representing control, a study of the cps transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.

[8] R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Twenty-second Annual ACM Symp. on Principles of Prog. Languages, pages 130–141, New York, Jan 1995. ACM Press.

[9] R. Harper and G. Morrisett. Typed closure conversion for recursively-defined functions. In Second International Workshop on Higher Order Operational Techniques in Semantics (HOOTS98, New York, Sep 1998. ACM Press.

[10] Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Proc. 23rd Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pages 271–283. ACM Press, 1996.

[11] G. Morrisett. Open problems for certifying compilers. Talk presented at 2000 PCC Workshop, Santa Barbara, CA, June 2000.

[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. Necula. Proof-carrying code. In Twenty-Fourth Annual ACM Symp. on Principles of Prog. Languages, New York, Jan 1997. ACM Press.

[14] S. Nettles and J. O’Toole. Real-time replication garbage collection. In Symposium on Programming Languages Design and Implementation, 1993.

[15] B. Saha, V. Trifonov, and Z. Shao. Fully reflexive intensional type analysis. Technical Report YALEU/DCS/TR-1194, Dept. of Computer Science, Yale University, New Haven, CT, March 2000.

[16] Z. Shao, C. League, and S. Monnier. Implementing typed intermediate languages. In Proc. 1998 ACM SIGPLAN International Conference on Functional Programming (ICFP’98), pages 313–323, September 1998.

[17] M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Proc. 21st Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pages 188–201. ACM Press, 1994.

[18] 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.

[19] V. Trifonov, B. Saha, and Z. Shao. Fully reflexive intensional type analsysis. In Proc. 2000 ACM SIGPLAN International Conference on Functional Programming (ICFP’00), pages 82–93. ACM Press, September 2000.

[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 (extended version). Technical Report TR-624-00, Princeton University, 2000.

[23] D. C. Wang and A. W. Appel. Type-preserving garbage collectors. In Proc. 28th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, page (to appear). ACM Press, 2001.

[24] P. Wilson. Uniprocessor garbage collection techniques. In 1992 International Workshop on Memory Management, New York, June 1992. ACM Press.

[25] P. R. Wilson. Uniprocessor garbage collection techniques.

Appendix

A. Soundness of λ_{GC}

Throughout this section, we assume unique variable names. Our environments are sets with no duplicate occurrences and no ordering. It is easy to show by induction over judgments that extending environments with additional bindings is safe. We will assume this in the rest of the section.

The code region cd is always implicitly part of the environment. We treat it as a constant region. Even when the environment is restricted to a particular set, say Ψ|_{Δ}, the code region is included in the restricted set. Therefore Ψ|_{ν_{1},...ν_{k}} is equivalent to {cd : Υcd, ν_{1} : Υ_{ν_{1}}, … ν_{k} : Υ_{ν_{k}}}. And Ψ|cd is equivalent to {cd : Υcd}.

Lemma A.1 If Δ′, r; Θ; Φ ⊢ σ, then Δ[ν/r]; Θ; Φ[ν/r] ⊢ σ[ν/r] where Δ′, r = Δ.

Proof The proof is a straightforward induction over the structure of σ.

Lemma A.2 (Φ[ν/r])|_{Δ,ν} = (Φ|_{Δ,r})[ν/r] and

(Γ[ν/r])|_{Δ,ν} = (Γ|_{Δ,r})[ν/r]

Proof The lemma is proved by considering the structure of Φ and Γ respectively, and comparing the results in the two cases.

Lemma A.3 If Ψ; Δ′, r; Θ; Φ; Γ ⊢ op : σ, then Ψ; Δ[ν/r]; Θ; Φ[ν/r]; Γ[ν/r] ⊢ op[ν/r] : σ[ν/r] where Δ′, r = Δ.

Proof The proof is by induction over the structure of op. Most of the cases follow directly by induction. We will show only the case for type packages. case ⟨α:Δ_{1} =σ_{1}, v:σ_{2}⟩: We know that

Ψ; Δ′, r; Θ; Φ; Γ ⊢ ⟨α:Δ_{1} =σ_{1}, v:σ_{2}⟩ : ∃α:Δ_{1}.σ_{2}

This implies that Δ_{1}; Θ; Φ|_{Δ_{1}} ⊢ σ_{1} and

Ψ; Δ′, r; Θ; Φ; Γ ⊢ v : σ_{2}[σ_{1}/α]

Suppose r ∉ Δ_{1}. Then r does not occur free in σ_{1}. Then applying the inductive hypothesis to the derivation for v, we get that

Ψ; Δ[ν/r]; Θ; Φ[ν/r]; Γ[ν/r] ⊢ v[ν/r] : (σ_{2}[ν/r])[σ_{1}/α]

Suppose Φ_{1} = Φ|_{Δ_{1}}. Then we have that Φ[ν/r]|_{Δ_{1}} = Φ_{1}, Φ_{2} and Dom(Φ_{1}) ∩ Dom(Φ_{2}) = ∅. Therefore, we have that

Δ_{1}; Θ; Φ|_{Δ_{1}}, Φ_{2} ⊢ σ_{1}

This implies that Δ_{1}; Θ; Φ[ν/r]|_{Δ_{1}} ⊢ σ_{1}, which leads to the required result.

Consider now that r ∈ Δ_{1}. Suppose Δ_{1} = Δ_{2}, r. Then

Δ_{2}, r; Θ; Φ|_{Δ_{2},r} ⊢ σ_{1}

Applying lemmas A.1 and A.2 we get that

Δ_{1}[ν/r]; Θ; (Φ[ν/r])|_{Δ_{2},ν} ⊢ σ_{1}[ν/r]

But Δ_{2}, ν = Δ_{1}[ν/r]. The second subderivation now becomes

Ψ; Δ′, r; Θ; Φ; Γ ⊢ v : σ_{2}[σ_{1}/α]

By applying the inductive hypothesis we get that

Ψ; Δ[ν/r]; Θ; Φ[ν/r]; Γ[ν/r] ⊢ v[ν/r] : (σ_{2}[ν/r])[σ_{1}[ν/r]/α]

This leads to the required result.

Lemma A.4 If Ψ; Δ′, r; Θ; Φ; Γ ⊢ e, then

Ψ; Δ[ν/r]; Θ; Φ[ν/r]; Γ[ν/r] ⊢ e[ν/r] where Δ′, r = Δ Proof The proof is by induction over the derivation of e. Most of the cases follow directly from the inductive hypothesis. We will consider only one case here. case only Δ_{1} ine: We get that

Ψ; Δ, r; Θ; Φ; Γ ⊢ only Δ_{1} ine

This implies that

Ψ|_{Δ_{1}}; Δ_{1}, cd; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}} ⊢ e

and Δ_{1} ⊂ Δ, r. Suppose r ∉ Δ_{1}. Then r does not occur free in e. Also Δ_{1}[ν/r] = Δ_{1}. Suppose Γ|_{Δ_{1}} = Γ_{1}. Then we have that Γ[ν/r]|_{Δ_{1}} = Γ_{1}, Γ_{2} and Dom(Γ_{1}) ∩ Dom(Γ_{2}) = ∅. Since we can extend environments, we get that Ψ|_{Δ_{1}}; Δ_{1}, cd; Θ; Φ_{1}, Φ_{2}; Γ_{1}, Γ_{2} ⊢ e, where Φ_{1} and Φ_{2} are constructed similar to Γ_{1} and Γ_{2}. This implies that

Ψ|_{Δ_{1}}; Δ_{1}, cd; Θ; Φ_{1}, Φ_{2}; Γ_{1}, Γ_{2} ⊢ e

Also Δ_{1} ⊂ (Δ, r)[ν/r]. This leads to the required result.

Suppose now that r ∈ Δ_{1}. Suppose that Δ_{1} = Δ_{2}, r. Then Δ_{1}[ν/r] = Δ_{2}, ν. Then we have that

Ψ|_{Δ_{2},r}; Δ_{2}, r, cd; Θ; Φ|_{Δ_{2},r}; Γ|_{Δ_{2},r} ⊢ e

Applying the inductive hypothesis we get that

Ψ|_{Δ_{2},r}; Δ_{1}[ν/r], cd; Θ; Φ|_{Δ_{2},r}[ν/r]; Γ|_{Δ_{2},r}[ν/r] ⊢ e[ν/r] Applying lemma A.2 we get that

Ψ|_{Δ_{2},r}; Δ_{1}[ν/r], cd; Θ; Φ[ν/r]|_{Δ_{2},ν}; Γ[ν/r]|_{Δ_{2},ν} ⊢ e[ν/r] But we have that Ψ|_{Δ_{2},r} = Ψ|_{Δ_{2}}. Moreover, Ψ|_{Δ_{2},ν} = Ψ|_{Δ_{2}}, Ψ′. Therefore, we get that

Ψ|_{Δ_{2},ν}; Δ_{1}[ν/r], cd; Θ; Φ[ν/r]|_{Δ_{2},ν}; Γ[ν/r]|_{Δ_{2},ν} ⊢ e[ν/r] We also have that Δ_{1}[ν/r] ⊂ Δ[ν/r]. This leads to the required result.

Lemma A.5 If Θ, t:κ′ ⊢ τ : κ and Θ ⊢ τ′ : κ′, then Θ ⊢ τ[τ′/t] : κ

Proof The proof is a straightforward induction over the structure of τ.

Lemma A.6 If Δ; Θ, t:κ; Φ ⊢ σ and Θ ⊢ τ : κ, then Δ; Θ; Φ ⊢ σ[τ/t]

Proof The proof is again a straighforward induction over the structure of σ.

Lemma A.7 If Ψ; Δ; Θ, t:κ; Φ; Γ ⊢ op : σ and Θ ⊢ τ : κ then Ψ; Δ; Θ; Φ; Γ[τ/t] ⊢ op[τ/t] : σ[τ/t]

Proof The proof is a straightforward induction over the structure of op. The only unusual case is when op = ν.ℓ. In this case, Ψ(ν.ℓ) = σ and Dom(Ψ); ·; · ⊢ σ. Therefore, the variable t does not occur free in σ atν.

Lemma A.8 If Ψ; Δ; Θ, t:κ; Φ; Γ ⊢ e and · ⊢ τ′ : κ then Ψ; Δ; Θ; Φ; Γ[τ′/t] ⊢ e[τ′/t]

Proof The proof is a straightforward induction over the structure of e. The only interesting case is for a typecase when the substituted variable is being analyzed. case typecase t of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃}): Suppose we substitute the type τ′ for the variable t. Then τ′ can only be one of Int, τ′′ → 0, τ′_{1} × τ′_{2}, or ∃t.τ′′. For a Int, we need to prove that

Ψ; Δ; Θ; Φ; Γ[Int/t] ⊢ (typecase t of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃}))[Int/t]

This implies that we need to prove that

Ψ; Δ; Θ; Φ; Γ[Int/t] ⊢ e_{i}[Int/t]

By definition, we know that

Ψ; Δ; Θ, t:Ω; Φ; Γ[Int/t] ⊢ e_{i}[Int/t]

Since t is being substituted away, this leads to the required result. For a code type we need to prove that

Ψ; Δ; Θ; Φ; Γ[τ′ → 0/t] ⊢

(typecase t of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃}))[τ′ → 0/t]

This implies that we need to prove that

Ψ; Δ; Θ; Φ; Γ[τ′ → 0/t] ⊢ e_{λ}[τ′ → 0/t]

By definition, we get that Ψ; Δ; Θ, t: Ω; Φ; Γ ⊢ e_{λ}. Substituting for t and applying the inductive hypothesis leads to the result.

For the pair type we need to prove that

Ψ; Δ; Θ; Φ; Γ[(τ′_{1} × τ′_{2})/t] ⊢

(typecase t of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃}))[(τ′_{1} × τ′_{2})/t]

This implies that we need to prove that

Ψ; Δ; Θ; Φ; Γ[(τ′_{1} × τ′_{2})/t] ⊢ e_{×}[(τ′_{1} × τ′_{2}), τ′_{1}, τ′_{2}/t, t_{1}, t_{2}]

By definition, we know that

Ψ; Δ; Θ, t:Ω, t_{1} :Ω, t_{2} :Ω; Φ; Γ[t_{1} × t_{2}/t] ⊢ e_{×}[t_{1} × t_{2}/t]

Note that the variables t_{1} and t_{2} do not occur free separately in Γ. Substituting τ′_{1} for t_{1}, τ′_{2} for t_{2}, and τ′_{1} × τ′_{2} for t_{1} × t_{2} leads to the required result.

For the existential type we need to prove that

Ψ; Δ; Θ; Φ; Γ[∃t_{1}.τ′/t] ⊢
(typecase t of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃}))[∃t_{1}.τ′/t]

This implies that we need to prove that

Ψ; Δ; Θ; Φ; Γ[∃t_{1}.τ′/t] ⊢ e_{∃}[∃t_{1}.τ′, λt_{1}.τ′/t, t_{e}]

By definition we know that

Ψ; Δ; Θ, t:Ω, t_{e}:Ω ⟶ Ω; Φ; Γ[∃t_{1}.t_{e}t_{1}/t] ⊢ e_{∃}[∃t_{1}.t_{e}t_{1}/t]

Substituting (λt_{1}.τ′) for t_{e} and applying the inductive hypothesis we get that

Ψ; Δ; Θ, t:Ω; Φ; Γ[∃t_{1}.τ′/t] ⊢ e_{∃}[∃t_{1}.τ′, λt_{1}.τ′/t, t_{e}]

Since t is being substituted away, we can remove it from the type environment. This leads to the required result.

Lemma A.9 If Δ; Θ; Φ, α:Δ′ ⊢ σ and Δ′; Θ; Φ ⊢ σ′, then Δ; Θ; Φ ⊢ σ[σ′/α]

Proof The proof is a straighforward induction over the structure of σ. In the case of c‘ode types, we use the fact that the argument types σ⃗ are fully closed.

Lemma A.10 If Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ op : σ and Δ′; Θ; Φ ⊢ σ′ then Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ op[σ′/α] : σ[σ′/α]

Proof The proof is again by induction over the typing derivation for op. We will consider only the case for packages. case ⟨β:Δ′ =σ_{1}, v:σ_{2}⟩: By definition,

Ψ; Δ; Θ; Φ, α:Δ_{1}; Γ ⊢ ⟨β:Δ′ =σ_{1}, v:σ_{2}⟩ : ∃β:Δ′.σ_{2}

There are two possible cases. If Δ_{1} ⊂ Δ′, then we get that Δ′; Θ; Φ|_{Δ′}, α:Δ_{1} ⊢ σ_{1} and Ψ; Δ; Θ; Φ, α:Δ_{1}; Γ ⊢ v : σ_{2}[σ_{1}/β] By lemma A.9, Δ′; Θ; Φ|_{Δ′} ⊢ σ_{1}[σ′/α] Applying the inductive hypothesis on the typing rule for v leads to the result.

In the other case, we get that Δ′; Θ; Φ|_{Δ′} ⊢ σ_{1} and Ψ; Δ; Θ; Φ, α:Δ_{1}; Γ ⊢ v : σ_{2}[σ_{1}/β] This implies that α does not occur free in σ_{1}. Therefore, we need to prove that

\begin{matrix}Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ \\ ⟨β:Δ′ =σ_{1}, v[σ′/α]:σ_{2}[σ′/α]⟩ : ∃β:Δ′.σ_{2}[σ′/α] \end{matrix}

This follows from applying the inductive hypothesis to the judgment for v.

Lemma A.11 If Δ; Θ; Φ ⊢ σ[σ′/α] and α occurs free in σ, then Δ; Θ; Φ ⊢ σ′

Proof The proof is by induction over the structure of σ.

Lemma A.12 If Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ e and Δ′; Θ; Φ ⊢ σ′ then

Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ e[σ′/α]

Proof The proof is again by induction over the derivation. The only non-trivial case is the only construct. case only Δ_{1} ine: By definition, Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ only Δ_{1} ine and Δ′; Θ; Φ ⊢ σ′. Suppose Δ′ ⊂ Δ_{1}. Then we get that

Ψ|_{Δ_{1}}; Δ_{1}, cd; Θ; Φ|_{Δ_{1}}, α:Δ′; Γ|_{Δ_{1}} ⊢ e

Applying the inductive hypothesis we get that

Ψ|_{Δ_{1}}; Δ_{1}, cd; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}}[σ′/α] ⊢ e[σ′/α]

But we also have that Γ|_{Δ_{1}}[σ′/α] = Γ[σ′/α]|_{Δ_{1}}. From here we can conclude that

Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ only Δ_{1} ine[σ′/α]

If Δ_{1} ⊂ Δ′, then we get that

Ψ|_{Δ_{1}}; Δ_{1}, cd; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}} ⊢ e

This implies that α does not occur free in e. We also have that Δ′; Θ; Φ ⊢ σ′. Using lemma A.11, we can show that Γ[σ′/α]|_{Δ_{1}} = Γ|_{Δ_{1}}. Therefore, we get that

Ψ|_{Δ_{1}}; Δ_{1}, cd; Θ; Φ|_{Δ_{1}}; Γ[σ′/α]|_{Δ_{1}} ⊢ e

This implies that

Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ only Δ_{1} ine

Lemma A.13 If Ψ; Δ; Θ; Φ; Γ, x:σ′ ⊢ op : σ and Ψ; Δ; Θ; Φ; Γ ⊢ v′ : σ′ then Ψ; Δ; Θ; Φ; Γ ⊢ op[v′/x] : σ

Proof The proof is a straightforward induction over the typing derivation for op.

Lemma A.14 If Ψ; Δ; Θ; Φ; Γ ⊢ v : σ and Δ_{1}; Θ; Φ|_{Δ_{1}} ⊢ σ and Δ_{1} ⊂ Δ, then Ψ|_{Δ_{1}}; Δ_{1}; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}} ⊢ v : σ Proof The proof is by induction over the derivation for v. Most of the cases follow directly from the inductive hypothesis. We will consider only one case here. case ν.ℓ: We have that Ψ; Δ; Θ; Φ; Γ ⊢ ν.ℓ : σ atν. This implies that Ψ(ν.ℓ) = σ and Dom(Ψ); ·; · ⊢ σ at ν. However, by assumption we also know that Δ_{1}; Θ; Φ|_{Δ_{1}} ⊢ σ atν. This implies that ν ∈ Δ_{1}. This implies that Ψ|_{Δ_{1}}(ν.ℓ) = σ. Moreover, we also get that Δ_{1}; ·; · ⊢ σ at ν. Therefore, we get that Dom(Ψ|_{Δ_{1}}); ·; · ⊢ σ at ν. From here we get that Ψ|_{Δ_{1}}; Δ_{1}; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}} ⊢ ν.ℓ : σ atν.

Lemma A.15 If Ψ; Δ; Θ; Φ; Γ, x:σ ⊢ e and Ψ; Δ; Θ; Φ; Γ ⊢ v : σ then Ψ; Δ; Θ; Φ; Γ ⊢ e[v/x]

Proof The proof is again a straightforward induction over the structure of e. We will only show the proof for a couple of cases, the rest of them follow similarly. case only Δ ine: We have that Ψ; Δ; Θ; Φ; Γ, x:σ ⊢ only Δ_{1} ine. This implies that Ψ|_{Δ_{1}}; Δ_{1}; Θ; Φ|_{Δ_{1}}; (Γ, x:σ)|_{Δ_{1}} ⊢ e. If we have that Δ_{1}; Θ; Φ|_{Δ_{1}} ⊢ σ, then we get that Ψ|_{Δ_{1}}; Δ_{1}; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}}, x:σ ⊢ e. By lemma A.14 we get that Ψ|_{Δ_{1}}; Δ_{1}; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}} ⊢ v : σ. Applying the inductive hypothesis gives us that Ψ|_{Δ_{1}}; Δ_{1}; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}} ⊢ e[v/x].

In the other case, we get that Ψ|_{Δ_{1}}; Δ_{1}; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}} ⊢ e. This implies that x does not occur free in e. The required result follows from here. case typecase t of (ei; e_{λ}; t_{1}t_{2}.e_{×}; t_{e}.e_{∃}): By assumption, we get

that Θ ⊢ t : Ω Ψ; Δ; Θ; Φ; Γ[Int/t], x:σ[Int/t] ⊢ e_{i}[Int/t] Ψ; Δ; Θ; Φ; Γ, x:σ ⊢ e_{λ} \begin{matrix}Ψ; Δ; Θ, t_{1} :Ω, t_{2} :Ω; Φ; Γ[t_{1} × t_{2}/t], x:σ[t_{1} × t_{2}/t] ⊢ \\ e_{×}[t_{1} × t_{2}/t] \end{matrix} \begin{matrix}Ψ; Δ; Θ, t_{e}:Ω ⟶ Ω; Φ; Γ[∃t_{1}.t_{e}t_{1}/t], x:σ[∃t_{1}.t_{e}t_{1}/t] ⊢ \\ e_{∃}[∃t_{1}.t_{e}t_{1}/t] \end{matrix}

By lemma A.7, we know that if Ψ; Δ; Θ; Φ; Γ ⊢ v : σ, then Ψ; Δ; Θ; Φ; Γ[τ/t] ⊢ v : σ[τ/t]. Now substitute v[Int/t] in the e_{i} branch, substitute v in the e_{λ} branch, substitute v[t_{1} × t_{2}/t] in the e_{×} branch, and substitute v[∃t_{1}.t_{e}t_{1}/t] in the e_{∃} branch. The required result follows from the inductive hypothesis on each branch.

Proposition A.16 (Type Preservation) If ⊢ (M, e) and (M, e) ⟹ (M′, e′) then ⊢ (M′, e′). Proof The proof is by induction over the evaluation relation. We will consider only the cases that do not follow directly from the inductive hypothesis and the substitution lemmas. case ν.ℓ[τ⃗][ν⃗](v⃗): The lemma follows from the fact that tag reduction is strongly normalizing and confluent, and that tag reduction preserves kind. case ν.ℓ[τ′][ν⃗](v⃗): By definition,

Ψ; Dom(Ψ); ·; ·; · ⊢ ν.ℓ[τ′][ν⃗](v⃗)

Since M(ν.ℓ) = (λ[t⃗:κ][r⃗](x⃗:σ⃗).e), we have that

Ψ; Dom(Ψ); ·; ·; · ⊢ ν.ℓ : ∀[t⃗:κ][r⃗](σ⃗) → 0 atν

This implies that

Ψ|cd; cd, r⃗; \overrightarrow{t:κ}; ·; \overrightarrow{x:σ} ⊢ e

By the typing rule, we get that

Ψ; Dom(Ψ); ·; ·; · ⊢ v_{i} : σ_{i}[ν⃗, τ′/r⃗, t⃗]

and · ⊢ τ′_{i} : κ_{i}. From lemma A.4 we get that

Ψ|cd; cd, ν⃗; Θ; ·; x⃗:σ[ν⃗/r⃗] ⊢ e[ν⃗/r⃗]

From lemma A.8 we get that

Ψ|cd; cd, ν⃗; ·; ·; x⃗:σ[ν⃗, τ′/r⃗, t⃗] ⊢ e[ν⃗, τ′/r⃗, t⃗]

Since Ψ|cd ⊂ Ψ and cd, ν⃗ ⊂ Dom(Ψ), we can extend the environment for deriving e. Applying lemma A.15 we get that

Ψ; Dom(Ψ); ·; ·; · ⊢ e[ν⃗, τ′, v⃗/r⃗, t⃗, x⃗]

which leads to the result. case (v⟦τ⃗⟧)[τ⃗][ν⃗](v⃗): By definition,

Ψ; Dom(Ψ); ·; ·; · ⊢ (v⟦τ⃗⟧)[τ⃗][ν⃗](v⃗)

From the typing rules Ψ; Dom(Ψ); ·; ·; · ⊢ (v⟦τ⃗⟧) : ∀⟦τ⃗⟧[r⃗](σ⃗) ⟶^{ν} 0 for some ν and Ψ; Dom(Ψ); ·; ·; · ⊢ v_{i} : σ_{i}[ν⃗/r⃗]. Again from the typing rules we get that Ψ; Dom(Ψ); ·; ·; · ⊢ v : ∀[t⃗:κ][r⃗](σ⃗′) → 0 atν where σ′_{i}[τ⃗/t⃗] = σ_{i} and · ⊢ τ_{i} : κ_{i}. We need to prove that

Ψ; Dom(Ψ); ·; ·; · ⊢ v[τ⃗][ν⃗](v⃗)

This is true if Ψ; Dom(Ψ); ·; ·; · ⊢ v_{i} : σ′_{i}[ν⃗, τ⃗/r⃗, t⃗]. But we already know that this holds. case letx = put[ν]v ine: By definition,

Ψ; Dom(Ψ); ·; ·; · ⊢ letx = put[ν]v ine

From the typing rules,

Ψ; Dom(Ψ); ·; ·; · ⊢ put[ν]v : σ atν

for some type σ, and ν ∈ Dom(Ψ). This implies that

Ψ; Dom(Ψ); ·; ·; · ⊢ v : σ

Again, from the typing rules,

Ψ, ν.ℓ:σ; Dom(Ψ); ·; ·; · ⊢ ν.ℓ : σ atν

The required result now follows from lemma A.15. case letx = get ν.ℓ ine: By definition,

Ψ; Dom(Ψ); ·; ·; · ⊢ letx = get ν.ℓ ine

From the typing rules we get that

Ψ; Dom(Ψ); ·; ·; · ⊢ ν.ℓ : σ atν

for some type σ Again from the typing rules, we get that Ψ(ν.ℓ) = σ. This implies that if M(ν.ℓ) = v, then

Ψ; Dom(Ψ); ·; ·; · ⊢ v : σ

The required result follows from lemma A.15. case open ⟨α:Δ=σ_{1}, v:σ_{2}⟩ as ⟨α, x⟩ in e: The two open constructs are proved similarly. We will show the proof for only one of them. By definition,

Ψ; Dom(Ψ); ·; ·; · ⊢ open ⟨α:Δ=σ_{1}, v:σ_{2}⟩ as ⟨α, x⟩ ine

This implies that

Ψ; Dom(Ψ); ·; α:Δ; x:σ_{2} ⊢ e

The required result follows from lemmas A.15 and A.12. case letregion r ine: By definition,

Ψ; Dom(Ψ); ·; ·; · ⊢ letregion r ine

This implies that

Ψ; Dom(Ψ), r; ·; ·; · ⊢ e

By lemma A.4,

Ψ; Dom(Ψ), ν; ·; ·; · ⊢ e[ν/r]

Since ν is a newly introduced region, we can extend Ψ with it. This implies that

Ψ, ν ↦ {}; Dom(Ψ), ν; ·; ·; · ⊢ e[ν/r]

This is the required result. case only Δ ine: By definition,

Ψ; Dom(Ψ); ·; ·; · ⊢ only Δ ine

This implies that

Ψ|_{Δ}; cd, Δ; ·; ·; · ⊢ e

But cd, Δ = Dom(Ψ|_{Δ}). This implies that

Ψ|_{Δ}; Dom(Ψ|_{Δ}); ·; ·; · ⊢ e

which is the required result.

For all of the typecases , the required result follows directly from the typing rules since the value environment is empty.

Lemma A.17 (Canonical forms)

1. If Ψ; Δ; ·; ·; · ⊢ v : intthen v = n.

2. If Ψ; Δ; ·; ·; · ⊢ v : σ atν then v = ν.ℓ.

3. If Ψ; Δ; ·; ·; · ⊢ v : σ_{1} × σ_{2} then v = (v_{1}, v_{2}).

4. If Ψ; Δ; ·; ·; · ⊢ v : ∃t:κ.σ then v = ⟨t=τ, v′:σ⟩.

5. If Ψ; Δ; ·; ·; · ⊢ v : ∃α:Δ′.σ then v = ⟨α:Δ′ =σ_{1}, v′:σ_{2}⟩.

6. If Ψ; Δ; ·; ·; · ⊢ v : ∀⟦τ⃗⟧[r⃗](σ⃗) ⟶^{ρ} 0 then v = v′⟦τ⃗⟧.

7. If Ψ; Δ; ·; ·; · ⊢ v : ∀[t⃗:κ][r⃗](σ⃗) → 0

then v = λ[t⃗:κ][r⃗](x⃗:σ).e.

Proof The proof follows from the inspection of the typing rules for values.

Proposition A.18 (Progress) If ⊢ (M, e) then either e = haltv or there exists a (M′, e′) such that (M, e) ⟹ (M′, e′). Proof The proof is again by induction over the structure of e. By definition, Ψ; Dom(Ψ); ·; ·; · ⊢ e. The proof for the individual cases start from this point. case v[τ⃗][ν⃗](v⃗): From the typing rules, either

v:∀[t⃗:κ][r⃗](σ⃗) → 0 atν or v:∀⟦τ⃗⟧[r⃗](σ⃗) ⟶^{ν} 0

In the first case by lemma A.17, v = ν.ℓ. From the typing rules M(ν.ℓ) = λ[t⃗:κ][r⃗](x⃗:σ).e This implies that we have a reduction. In the second case, by lemma A.17 v = v′⟦τ⟧. In this case also

we have a reduction to v′[τ⃗][ν⃗](v⃗).

case let x = op in e: If op = v, then we have a reduction. If op = π_{i}v, then from the typing rules, Ψ; Dom(Ψ); ·; ·; · ⊢ v : σ_{1} × σ_{2}. The required result follows from lemma A.17. In the case of put[ν]v, the result follows directly. The constraint ν ∈ Δ ensures that ν ∈ Dom(Ψ). In the case for get v, by the typing rules we know that v = ν.ℓ for some ν.ℓ. Again from the typing rule we know that Ψ(ν.ℓ) = σ. This implies that M(ν.ℓ) = v′ for some value v′.

For the other cases of e, the proposition follows directly from the operational semantics.

— Syntactic type shorthands for notational convenience: — t_{c}[t] ≡ ∀⟦t_{1}, t_{2}, t_{e}⟧[r_{1}, r_{2}, r_{3}](M_{r_{2}}(t), α_{c}) ⟶^{ρ} 0 × α_{c} — Basic type of the continuations of copy — t_{k}[t] ≡ (∃t_{1} :Ω.∃t_{2} :Ω.∃t_{e}:Ω ⟶ Ω.∃α_{c}:{r_{1}, r_{2}, r_{3}}.t_{c}[t]) atr_{3} — Same as t_{c} but closed with existential packages —

— The main GC entry point — fixgc[t:Ω][r_{1}](f:∀[][r](M_{r}(t)) → 0, x:M_{r_{1}}(t)).

letregion r_{2} in

letregion r_{3} in

letc = (gcend⟦t, int, λt.t⟧, f) in

letk = put[r_{3}]⟨t_{1} =t, t_{2} =int, t_{e} =λt.t, α_{c}:{r_{1}, r_{2}, r_{3}} = ∀[][r](M_{r}(t)) → 0, c:t_{c}[t]⟩ in copy[t][r_{1}, r_{2}, r_{3}](x, k)

— The second half of GC, passed as a continuation to copy — fixgcend[t_{1} :Ω, t_{2} :Ω, t_{e}:Ω ⟶ Ω][r_{1}, r_{2}, r_{3}](y:M_{r_{2}}(t_{1}), f:∀[][r](M_{r}(t_{1})) → 0).

only {r_{2}} inf[][r_{2}](y)

— The main copy entry point — fixcopy[t:Ω][r_{1}, r_{2}, r_{3}](x:M_{r_{1}}(t), k:t_{k}[t]).

typecase t of

int ⇒ open (get k) as ⟨t_{1}, t_{2}, t_{e}, α_{c}, c⟩ in(π_{1}c)[t_{1}, t_{2}, t_{e}][r_{1}, r_{2}, r_{3}](x, π_{2}c)
λ ⇒ open (get k) as ⟨t_{1}, t_{2}, t_{e}, α_{c}, c⟩ in(π_{1}c)[t_{1}, t_{2}, t_{e}][r_{1}, r_{2}, r_{3}](x, π_{2}c)

t_{1} × t_{2} ⇒ letc = (copypair1⟦t_{1}, t_{2}, λt.t⟧, (π_{2}(get x), k)) in

letk = put[r_{3}]⟨t_{1} =t_{1}, t_{2} =t_{2}, t_{e} =λt.t, α_{c}:{r_{1}, r_{2}, r_{3}} = M_{r_{1}}(t_{2}) × t_{k}[t], c:t_{c}[t_{1}]⟩ in
copy[t_{1}][r_{1}, r_{2}, r_{3}](π_{1}(get x), k)

∃t_{e} ⇒ open (get x) as ⟨t_{x}, y⟩ in

letc = (copyexist1⟦t_{x}, int, t_{e}⟧, k) in
letk = put[r_{3}]⟨t_{1} =t_{x}, t_{2} =int, t_{e} =t_{e}, α_{c}:{r_{1}, r_{2}, r_{3}} = t_{k}[t], c:t_{c}[t_{e}t_{1}]⟩ in
copy[t_{e}t_{x}][r_{1}, r_{2}, r_{3}](y, k)

— First continuation when copying a pair — fixcopypair1[t_{1} :Ω, t_{2} :Ω, t_{e}:Ω ⟶ Ω][r_{1}, r_{2}, r_{3}](x_{1} :M_{r_{2}}(t_{1}), c:M_{r_{1}}(t_{2}) × t_{k}[t_{1} × t_{2}]).

letc′ = (copypair2⟦t_{2}, t_{1}, λt.t⟧, (x_{1}, π_{2}c,)) in

letk = put[r_{3}]⟨t_{1} =t_{1}, t_{2} =t_{2}, t_{e} =λt.t, α_{c}:{r_{1}, r_{2}, r_{3}} = M_{r_{2}}(t_{1}) × t_{k}[t_{1} × t_{2}], c′:t_{c}[t_{2}]⟩ in copy[t_{2}][r_{1}, r_{2}, r_{3}](π_{1}c, k)

— Second continuation when copying a pair — fixcopypair2[t_{1} :Ω, t_{2} :Ω, t_{e}:Ω ⟶ Ω][r_{1}, r_{2}, r_{3}](x_{2} :M_{r_{2}}(t_{2}), c:M_{r_{2}}(t_{1}) × t_{k}[t_{1} × t_{2}]).

open (get (π_{2}c)) as ⟨t_{1}, t_{2}, t_{e}, α_{c}, c′⟩ in(π_{1}c′)[t_{1}, t_{2}, t_{e}][r_{1}, r_{2}, r_{3}](put[r_{2}](π_{1}c, x_{2}), π_{2}c′)

— Continuation when copying an existential package — fixcopyexist1[t_{1} :Ω, t_{2} :Ω, t_{e}:Ω ⟶ Ω][r_{1}, r_{2}, r_{3}](z:M_{r_{2}}(t_{e}t_{1}), c:t_{k}[t_{e}t_{1}]).

open (get c) as ⟨t′_{1}, t′_{2}, t′_{e}, α′_{c}, c′⟩ in(π_{1}c′)[t′_{1}, t′_{2}, t′_{e}][r_{1}, r_{2}, r_{3}](put[r_{2}]⟨t=t_{1}, z:M_{r_{2}}(t_{e}t)⟩, π_{2}c′)

Figure 12: The basic GC code after CPS and closure conversion.

B. Closed CPS garbage collector

Figure 12 presents the code of the basic collector after CPS and closure conversion (the direct-style code is shown in Fig. 4). The presence of free tag variables in the continuations requires the use of a form of translucent types for the typed closure conversion [10].

In the general case typed closure conversion also requires existential quantification over kinds, but in the present case, we can avoid it by using a superset of all possible kinds: since some continuations require t_{1}, t_{2} of kind Ω, Ω while others only need t_{1}, t_{e} or kind Ω, (Ω → Ω), we unify the two into t_{1}, t_{2}, t_{e} where some of the arguments are simply left unused.

The verbose type annotations make it look more scary than it really is. Four new functions were introduced because of CPS conversion. They are all used as continuations to calls to copy:

1. gcend is the code executed at the end of the toplevel call to copy and just finishes the garbage collection by freeing the from space and calling back the mutator.

2. copyexist1 is the continuation of the recursive call to copy an

existential package.

3. Since copying a pair requires two recursive calls, we need both copypair1 for the continuation of the first call and copypair2 for the continuation of the second.

Since the code has to be closed, all the free variables need to be passed explicitly via the continuation object k whose type is abbreviated as t_{k}[t] but is really a big existential wrapper around the real data whose type is abbreviated as t_{c}[t].

C. Soundness of λ_{GCforw}

As before, We use the usual exchange and weakening properties of environments without proving them. The code region cd is always implicitly part of the environment. Even when the environment is restricted to a particular set, say Ψ|_{Δ}, the code region is included in the restricted set.

We will show the proofs only for the extensions. The only nontrivial extension is the widen construct. The proofs of the propositions for the other constructs follow in a straightforward way by induction over the derivations.

Because of the widen operator, the notion of a well formed machine state has to be slightly adjusted to allow non-well-formed memory elements as long as they can be shown not to influence the execution:

Definition C.1 The machine state (M, e) is well formed iff

{\overline{M} ⊂ M  ⊢ \overline{M}:Ψ  Ψ; Dom(Ψ); ·; ·; · ⊢ e \atop ⊢ (M, e)}

Note that to show well-formedness we now need to find not only a witness Ψ but also a proper \overline{M} subset.

The reason is that widen casts the whole live heap from one type to the other but cannot cast any arbitrary M because it might include existential packages of the form ⟨α:Δ=σ_{1}, v:σ_{2}⟩ where casting α would require an update of M, which goes against the idea that widen is a nop.

This problem appears when we try to prove type preservation, which is the main obstacle to show soundness of the widen operator, whose proof uses two lemmas for the following two steps:

1. First, we construct a \overline{M} which only contains elements that we can cast (i.e. of type M_{ρ}(τ)) and we show that the state is still well-formed. This is the case because when we reach a widen, all the live data if of such a type.

2. Then we show that when everything has a type of the form M_{ρ}(τ), we can cast every single type consistently to its C_{ρ,ρ′}(τ) equivalent and the result is still properly typed. This relies on the subsumption rule on sum types and the fact that C types only differs from Mtypes by adding branches to sum types.

Lemma C.2 (Region Substitution)

1. If Ψ; Δ, r; Θ; Φ; Γ ⊢ op : σ then Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ op[ν/r] : σ[ν/r].

2. If Ψ; Δ, r; Θ; Φ; Γ ⊢ e then Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ e[ν/r].

Proof Straightforward proof via induction over the derivation of the typing judgment. Note that ν ∈ Ψ is not required here. case letx = widen[ρ′][τ](v) ine: We have that Ψ; Δ, r; Θ; Φ; Γ ⊢ letx = widen[ρ′][τ](v) ine. This implies Ψ; Δ, r; Θ; Φ; Γ ⊢ v : M_{ρ}(τ) and Ψ|cd; cd, ρ, ρ′; Θ; Φ|_{ρρ′}; x:C_{ρ,ρ′}(τ) ⊢ e. Applying lemma C.2.1 to the derivation for v we get that Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ v[ν/r] : M_{ρ[ν/r]}(τ) since M_{ρ}(τ)[ν/r] = M_{ρ[ν/r]}(τ).

If either ρ = r or ρ′ = r then the inductive hypothesis on the derivation of e and lemma A.2 and the fact that C_{ρ,ρ′}(τ)[ν/r] = C_{(ρ,ρ′)[ν/r]}(τ) leads to the required result.

In the other case, Φ[ν/r]|_{ρρ′} = Φ|_{ρρ′}, Φ′ where Dom(Φ|_{ρρ′}) ∩ Dom(Φ′) is empty. Moreover, r does not occur free in e. Since we can extend environments with new bindings we get that Ψ|cd; cd, ρ, ρ′; Θ; Φ|_{ρρ′}, Φ′; x:C_{ρ,ρ′}(τ) ⊢ e. This leads to the required result.

Lemma C.3 (Type Substitution)

1. If Ψ; Δ; Θ, t:κ; Φ; Γ ⊢ op : σ and Θ ⊢ τ : κ then Ψ; Δ; Θ; Φ; Γ[τ/t] ⊢ op[τ/t] : σ[τ/t].

2. If Ψ; Δ; Θ, t:κ; Φ; Γ ⊢ e and Θ ⊢ τ : κ then Ψ; Δ; Θ; Φ; Γ[τ/t] ⊢ e[τ/t].

3. If Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ op : σ and Δ′; Θ; Φ ⊢ σ′ then Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ op[σ′/α] : σ[σ′/α]

4. If Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ e and Δ′; Θ; Φ ⊢ σ′ then Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ e[σ′/α]

Proof Same thing here, the induction hypothesis can always be applied directly.

Lemma C.4 (Value Substitution)

1. If Ψ; Δ; Θ; Φ; Γ, x:σ ⊢ op : σ′ and Ψ; Δ; Θ; Φ; Γ ⊢ v : σ then Ψ; Δ; Θ; Φ; Γ ⊢ op[v/x] : σ′.

2. If Ψ; Δ; Θ; Φ; Γ, x:σ ⊢ e and Ψ; Δ; Θ; Φ; Γ ⊢ v : σ then Ψ; Δ; Θ; Φ; Γ ⊢ e[v/x].

Proof The proof is by induction over the derivation of the type judgment. Most of the cases follow directly from the induction hypothesis. Exceptions are:

widen We need to show that the substitution on e has no effect, which is easy since the variable we are substituting cannot occur freely in e.

Definition C.5 Let Ψ|_{ν,M} be the restriction of Ψ to pieces of code or elements of type M_{ν}(τ):

Ψ|_{ν′,M} = \{ν.ℓ:σ | Ψ(ν.ℓ) = σ ∧ (\begin{matrix}σ = ∀[τ⃗][r⃗](\overrightarrow{v:σ}) → 0 \\ ∨ ∃τ.(σ atν = M_{ν′}(τ)) \end{matrix})\}

Note that since cd only contains functions, Ψ|_{ν,M} will preserve all its contents.

Lemma C.6 If Ψ; Dom(Ψ); ·; ·; · ⊢ v : M_{ν}(τ) then Ψ|_{ν,M}; Dom(Ψ|_{ν}); ·; ·; · ⊢ v : M_{ν}(τ)

Proof By the definition of the Mtype, v is either of type intor of type σ atν. The lemma follows trivially if v is of type int. Consider the other cases. case M_{ν}(τ → 0): In this case v = cd.ℓ. Therefore Ψ(cd.ℓ) = ∀[][r](M_{r}(τ)) → 0. Therefore M(cd.ℓ) = λ[][r](\overrightarrow{x:σ}).e. The lemma now follows since the body e is typed only under the code region Ψ|cd and the region environment cd, r. case M_{ν}(τ_{1} × τ_{2}): We again have that v = ν.ℓ. Therefore, Ψ(ν.ℓ) = left(M_{ν}(τ_{1}) × M_{ν}(τ_{2})). This implies that M(ν.ℓ) = inlv′. We know that

Ψ; Dom(Ψ); ·; ·; · ⊢ inlv′ : left(M_{ν}(τ_{1}) × M_{ν}(τ_{2})) This implies that

Ψ; Dom(Ψ); ·; ·; · ⊢ v′ : (M_{ν}(τ_{1}) × M_{ν}(τ_{2})) This implies that v′ = (v′_{1}, v′_{2}). From the typing rules we get that Ψ; Dom(Ψ); ·; ·; · ⊢ v′_{1} : M_{ν}(τ_{1}) and Ψ; Dom(Ψ); ·; ·; · ⊢ v′_{2} : M_{ν}(τ_{2}). Applying the inductive hypothesis to the derivations for v′_{1} and v′_{2}, we get that Ψ|_{ν,M}; Dom(Ψ|_{ν}); ·; ·; · ⊢ v′_{1} : M_{ν}(τ_{1}) and Ψ|_{ν,M}; Dom(Ψ|_{ν}); ·; ·; · ⊢ v′_{2} : M_{ν}(τ_{2}). The required result follows from this. case M_{ν}(∃t.τ): We again have that v = ν.ℓ. Therefore, Ψ(ν.ℓ) = left(∃t.M_{ν}(τ)). This implies that M(ν.ℓ) = inlv′. We know that

Ψ; Dom(Ψ); ·; ·; · ⊢ inlv′ : left(∃t.M_{ν}(τ))

This implies that

Ψ; Dom(Ψ); ·; ·; · ⊢ v′ : ∃t.M_{ν}(τ)

This implies that v′ = ⟨t=τ′, v′′:M_{ν}(τ)⟩. From here we get that Ψ; Dom(Ψ); ·; ·; · ⊢ v′′ : (M_{ν}(τ))[τ′/t]. But we have that (M_{ν}(τ))[τ′/t] = M_{ν}(τ[τ′/t]). Therefore, applying the inductive hypothesis to the derivation for v′′, we get that Ψ|_{ν,M}; Dom(Ψ|_{ν}); ·; ·; · ⊢ v′′ : M_{ν}(τ[τ′/t]). The required result follows from this.

Definition C.7 Let T_{ρ,ρ′} be the type operator that turns a type of the form M_{ρ}(τ) into a type of the form C_{ρ,ρ′}(τ) and keeps code pointer types unchanged:

\begin{matrix}T_{ρ,ρ′}(M_{ρ}(τ)) = C_{ρ,ρ′}(τ) \\ T_{ρ,ρ′}(∀[τ⃗][r⃗](\overrightarrow{v:σ}) → 0 atρ) = ∀[τ⃗][r⃗](\overrightarrow{v:σ}) → 0 atρ \end{matrix}

We also use this operator on Ψ where it is defined as:

T_{ρ,ρ′}(Ψ) = {ν.ℓ:σ | Ψ(ν.ℓ) = σ′ ∧ T_{ρ,ρ′}(σ′ atρ) = σ atρ}

Note that the two parts of the definition of T_{ρ,ρ′}(σ) overlap but are consistent since M_{ρ}(τ) and C_{ρ,ρ′}(τ) are identical in the case when τ is an arrow type. Also, since cd only contains functions, T_{ρ,ρ′}(Ψ) does not change the type of cd. Finally since both Mand C are iterators, the T type operator can be defined as an iterator.

Lemma C.8 If Ψ|_{ν,M}; Dom(Ψ|_{ν}); ·; ·; · ⊢ v : M_{ν}(τ), then T_{ν,ν′}(Ψ|_{ν,M}); Dom(Ψ|_{ν}), ν′; ·; ·; · ⊢ v : C_{νν′}(τ)

Proof When v is of type int, the lemma follows trivially. case M_{ν}(τ → 0): In this case v = cd.ℓ and M(cd.ℓ) = λ[][r](\overrightarrow{x:σ}).e. This implies that Ψ|cd; cd, r; ·; ·; \overrightarrow{x:σ} ⊢ e. Since M_{ν}(τ′ → 0) = C_{νν′}(τ′ → 0) the type operator T is the identity for code types. Therefore, the cast will leave the type of the code region unchanged. Therefore Ψ|cd = (T_{ν,ν′}(Ψ|_{ν,M}))|cd. This leads to the required result. case M_{ν}(τ_{1} × τ_{2}): We again have that v = ν.ℓ. Therefore, Ψ(ν.ℓ) = left(M_{ν}(τ_{1}) × M_{ν}(τ_{2})). This implies that M(ν.ℓ) = inlv′. We know that

Ψ; Dom(Ψ); ·; ·; · ⊢ inlv′ : left(M_{ν}(τ_{1}) × M_{ν}(τ_{2}))

This implies that

Ψ; Dom(Ψ); ·; ·; · ⊢ v′ : (M_{ν}(τ_{1}) × M_{ν}(τ_{2}))

This implies that v′ = (v′_{1}, v′_{2}). From the typing rules we get that Ψ; Dom(Ψ); ·; ·; · ⊢ v′_{1} : M_{ν}(τ_{1}) and Ψ; Dom(Ψ); ·; ·; · ⊢ v′_{2} : M_{ν}(τ_{2}). Applying lemma C.6 to the derivations for v′_{1} and v′_{2}, we get that Ψ|_{ν,M}; Dom(Ψ|_{ν}); ·; ·; · ⊢ v′_{1} : M_{ν}(τ_{1}) and Ψ|_{ν,M}; Dom(Ψ|_{ν}); ·; ·; · ⊢ v′_{2} : M_{ν}(τ_{2}). Applying the inductive hypothesis to the derivations for v′_{1} and v′_{2} we get that T_{ν,ν′}(Ψ|_{ν,M}); Dom(Ψ|_{ν}), ν′; ·; ·; · ⊢ v′_{1} : C_{νν′}(τ_{1}) and T_{ν,ν′}(Ψ|_{ν,M}); Dom(Ψ|_{ν}), ν′; ·; ·; · ⊢ v′_{2} : C_{νν′}(τ_{2}). From here we can conclude that

T_{ν,ν′}(Ψ|_{ν,M}); Dom(Ψ|_{ν}), ν′; ·; ·; · ⊢
inlv′ : left(C_{νν′}(τ_{1}) × C_{νν′}(τ_{2}))

By the subtyping rule we can conclude that T_{ν,ν′}(Ψ|_{ν,M}); Dom(Ψ|_{ν}), ν′; ·; ·; · ⊢

inlv′ : (+\begin{matrix}left(C_{νν′}(τ_{1}) × C_{νν′}(τ_{2})) \\ right(M_{ν′}(τ_{2} × τ_{2})) \end{matrix})

This is the required result.

case M_{ν}(∃t.τ): The proof proceeds exactly as in the previous case. We only need to use the fact that (C_{ρ,ρ′}(τ))[τ′/t] = C_{ρ,ρ′}(τ[τ′/t])

Proposition C.9 (Type Preservation)

If ⊢ (M, e) and (M, e) ⟹ (M′, e′) then ⊢ (M′, e′).

Proof The proof is by cases on the structure of e. For each possible case, we use the typing derivation together with the evaluation step to get the derivation of the new typing judgment. This mostly relies on the substitution lemmas. We only show the more interesting cases.

• (M, letx = v ine) ⟹ (M, e[v/x])

From ⊢ (M, letx = v ine) we get that ⊢ \overline{M}:Ψ and Ψ; Dom(Ψ); ·; ·; · ⊢ letx = v ine. The derivation in turns tells us that Ψ; Dom(Ψ); ·; ·; · ⊢ v : σ and Ψ; Dom(Ψ); ·; ·; ·, x:σ:⊢ e. At this point, we can apply value substitution to get Ψ; Dom(Ψ); ·; ·; · ⊢ e[v/x].

• (M, only Δ ine) ⟹ (M|_{Δ}, e)

Here we get Ψ; Dom(Ψ); ·; ·; · ⊢ only Δ ine which gives us Ψ|_{Δ}; Δ; ·; ·; · ⊢ e. Since \overline{M} ⊂ M, we have that \overline{M}|_{Δ} ⊂ M|_{Δ}. Moreover, we know that Δ ⊂ Dom(Ψ). Therefore, Dom(Ψ|_{Δ}) = Δ.

• (M, letx = widen[ν′][τ](v) ine) ⟹ (M, e[v/x]) We know that if \overline{M}:Ψ, then we have that Ψ; Dom(Ψ); ·; ·; · ⊢ letx = widen[ν′][τ](v) ine. This implies that Ψ; Dom(Ψ); ·; ·; · ⊢ v : M_{ν}(τ) and Ψ|cd; cd, ν, ν′; ·; ·; , x:C_{νν′}(τ) ⊢ e for some ν and ν′ belonging to Dom(Ψ). By lemma C.6 we have that Ψ|_{ν,M}; Dom(Ψ|_{ν}); ·; ·; · ⊢ v : M_{ν}(τ). By lemma C.8 we have that T_{ν,ν′}(Ψ|_{ν,M}); Dom(Ψ|_{ν}); ·; ·; · ⊢ v : C_{νν′}(τ). But we have that T_{ν,ν′}(Ψ|_{ν,M}) = Ψ|cd, Ψ′ for some Ψ′ since the cast leaves the code type unchanged. Also Ψ′ = T_{νν′}(Ψ|_{ν,M}) Since we can extend the environment, we have that Ψ|cd, Ψ′; cd, ν, ν′; ·; ·; , x:C_{νν′}(τ) ⊢ e. Applying lemma C.4.2 we get that Ψ|cd, Ψ′; cd, ν, ν′; ·; ·; · ⊢ e[v/x]. This implies that Ψ|cd, Ψ′, ν′ ↦ {}; cd, ν, ν′; ·; ·; · ⊢ e[v/x]. If \overline{M}:Ψ|cd, Ψ′, ν′ ↦ \{\}, then clearly \overline{M} ⊂ M. This leads to the required result.

Lemma C.10 (Canonical forms)

1. If Ψ; Δ; ·; ·; · ⊢ v : intthen v = n.

2. If Ψ; Δ; ·; ·; · ⊢ v : σ atρ then v = ν.ℓ.

3. If Ψ; Δ; ·; ·; · ⊢ v : σ_{1} × σ_{2} then v = (v_{1}, v_{2}).

4. If Ψ; Δ; ·; ·; · ⊢ v : ∃t.σ then v = ⟨t=τ, v′:σ⟩.

5. If Ψ; Δ′; ·; ·; · ⊢ v : ∃α:Δ.σ then v = ⟨α:Δ=σ_{1}, v′:σ_{2}⟩.

6. If Ψ; Δ; ·; ·; · ⊢ v : ∀⟦τ⃗⟧[r⃗](σ⃗) ⟶^{ρ} 0 then v = v′⟦τ⃗⟧.

7. If Ψ; Δ; ·; ·; · ⊢ v : ∀[t⃗:κ][r⃗](σ⃗) → 0

then v = λ[t⃗:κ][r⃗](x⃗:σ).e.

Proof The proof follows from the inspection of the typing rules for values.

Proposition C.11 (Progress) If ⊢ (M, e) then either e = haltv or there exists a (M′, e′) such that (M, e) ⟹ (M′, e′). Proof The proof is again by cases on the structure of e. It uses lemma C.10.

D. Soundness of λ_{GCgen}

In this section, we prove the soundness of λ_{GCgen}. We will prove soundness in the same way – with the subject reduction and progress lemmas. Since λ_{GCgen} is just an extension of λ_{GC}, we will prove the required lemmas only for the new cases. As usual we will use the exchange and widening lemmas for environments throughout the section.

Lemma D.1 If Δ; Θ; Φ ⊢ σ, then Δ[ν/r]; Θ; Φ[ν/r] ⊢ σ[ν/r].

Proof The proof is by induction over the derivation of σ.

Lemma D.2 (Φ[ν/r])|_{Δ,ν} = (Φ|_{Δ,r})[ν/r] and (Γ[ν/r])|_{Δ,ν} = (Γ|_{Δ,r})[ν/r]

Proof Same as lemma A.2.

Lemma D.3 (M_{ρ_{1},ρ_{2}}(τ))[τ′/t] = M_{ρ_{1},ρ_{2}}(τ[τ′/t]) and (M_{ρ_{1},ρ_{2}}(τ))[ν/r] = M_{ρ_{1}[ν/r],ρ_{2}[ν/r]}(τ)

Proof Proved by considering the different possible reductions of M_{ρ_{1},ρ_{2}}(τ).

Lemma D.4 If Ψ; Δ, r; Θ; Φ; Γ ⊢ op : σ, then Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ op[ν/r] : σ[ν/r]

Proof The proof is a straightforward induction over the derivation for op. Note that Δ, ν = (Δ, r)[ν/r]. It uses lemma D.3 for the case involving subtyping with the M_{ρ_{1},ρ_{2}}(τ) type. case ⟨r′ ∈ Δ′ = ρ, v⟩: We have that

Ψ; Δ, r; Θ; Φ; Γ ⊢ ⟨r′ ∈ Δ′ = ρ, v⟩ : ∃r′ ∈Δ′.(σ atr′)

This implies that Ψ; Δ, r; Θ; Φ; Γ ⊢ v : σ[ρ/r′] atρ and ρ ∈ Δ′ and Δ′ ⊂ Δ, r. Applying the inductive hypothesis we get that

Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ v[ν/r] : (σ[ρ/r′])[ν/r] atρ[ν/r]

This implies that

\begin{matrix}Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ \\ v[ν/r] : (σ[ν/r])[(ρ[ν/r])/r′] atρ[ν/r] \end{matrix}

Moreover, Δ′[ν/r] ⊂ Δ, ν and ρ[ν/r] ∈ Δ′[ν/r]. This implies that

Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ ⟨r′ ∈ Δ′[ν/r] = ρ[ν/r], v[ν/r]⟩ : ∃r′ ∈{Δ′[ν/r]}.(σ[ν/r] atr′)

Lemma D.5 If Ψ; Δ, r; Θ; Φ; Γ ⊢ e, then Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ e[ν/r] Proof The proof is by induction over the derivation of e. Note that Δ, ν = (Δ, r)[ν/r]. We will consider only the extra cases here. case open v as ⟨r′, x⟩ ine: We have that

Ψ; Δ, r; Θ; Φ; Γ ⊢ open v as ⟨r′, x⟩ ine

This implies that

Ψ; Δ, r, r′; Θ; Φ; Γ, x:σ atr′ ⊢ e

and Ψ; Δ, r; Θ; Φ; Γ ⊢ v : ∃r′ ∈Δ′.(σ atr′). Applying lemma D.4 to the derivation for v we get that

Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ v[ν/r] : ∃r′ ∈Δ′[ν/r].(σ[ν/r] atr′)

Applying the inductive hypothesis to the derivation for e we get that

Ψ; Δ, ν, r′; Θ; Φ[ν/r]; Γ[ν/r], x:σ[ν/r] atr′ ⊢ e[ν/r]

From this we get that

Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ open v[ν/r] as ⟨r′, x⟩ ine[ν/r]

case ifreg (r_{1} = r_{2}) e_{1} e_{2}: We have that

\begin{matrix}Ψ; (Δ, r)[r′, r′/r_{1}, r_{2}]; Θ; Φ[r′, r′/r_{1}, r_{2}]; Γ[r′, r′/r_{1}, r_{2}] ⊢ \\ e_{1}[r′, r′/r_{1}, r_{2}] \end{matrix}

and Ψ; Δ, r; Θ; Φ; Γ ⊢ e_{2} and r′ ∉ Δ, r. Applying the inductive hypothesis to the derivation for e_{2} leads to

Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ e_{2}[ν/r]

Applying the inductive hypothesis to the derivation for e_{1} and using the fact that r is different from r_{1} and r_{2} we get that

Ψ; (Δ, ν)[r′, r′/r_{1}, r_{2}]; Θ;
(Φ[ν/r])[r′, r′/r_{1}, r_{2}]; (Γ[ν/r])[r′, r′/r_{1}, r_{2}] ⊢
(e_{1}[ν/r])[r′, r′/r_{1}, r_{2}]

This leads to the required result.

case ifreg (r = r_{2}) e_{1} e_{2}: We have that

Ψ; Δ, r; Θ; Φ; Γ ⊢ ifreg (r = r_{2}) e_{1} e_{2}

This implies that

\begin{matrix}Ψ; (Δ, r)[r′, r′/r, r_{2}]; Θ; Φ[r′, r′/r, r_{2}]; Γ[r′, r′/r, r_{2}] ⊢ \\ e_{1}[r′, r′/r, r_{2}] \end{matrix}

and Ψ; Δ, r; Θ; Φ; Γ ⊢ e_{2}. We must prove that

Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ ifreg (ν = r_{2}) e_{1}[ν/r] e_{2}[ν/r]

This implies that we must prove that Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ e_{2}[ν/r] and

\begin{matrix}Ψ; (Δ, ν)[ν/r_{2}]; Θ; (Φ[ν/r])[ν/r_{2}]; (Γ[ν/r])[ν/r_{2}] ⊢ \\ (e_{1}[ν/r])[ν/r_{2}] \end{matrix}

This implies that we must prove that

\begin{matrix}Ψ; (Δ, r)[ν, ν/r, r_{2}]; Θ; Φ[ν, ν/r, r_{2}]; Γ[ν, ν/r, r_{2}] ⊢ \\ e_{1}[ν, ν/r, r_{2}] \end{matrix}

Applying the inductive hypothesis to the derivation for e_{2} leads to the required result for this derivation. In the case for e_{1}, we substitute for r′ and applying the inductive hypothesis and the fact that r′ ∉ Δ, r leads to the required result. case ifreg (ν′ = r_{2}) e_{1} e_{2}: This case follows directly from the inductive hypothesis on the derivations of e_{1} and e_{2} and using the fact that ν′ ≠ ν and r ≠ r_{2}. case ifreg (ν = r_{2}) e_{1} e_{2}: This case follows directly from the inductive hypothesis on the derivations of e_{1} and e_{2} and using the fact that r ≠ r_{2}. case ifreg (ν′ = r) e_{1} e_{2}: We have that

Ψ; Δ, r; Θ; Φ; Γ ⊢ ifreg (ν′ = r) e_{1} e_{2}

This means that we know that

Ψ; Δ, r; Θ; Φ; Γ ⊢ e_{2}

We have to prove that

Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ ifreg (ν′ = ν) e_{1}[ν/r] e_{2}[ν/r]

This implies that we have to prove that

Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ e_{2}[ν/r]

Applying the inductive hypothesis to the derivation for e_{2} leads to the result. case ifreg (ν = r) e_{1} e_{2}: We have that

Ψ; Δ, r; Θ; Φ; Γ ⊢ ifreg (ν = r) e_{1} e_{2}

This means that we know that

Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ e_{1}[ν/r]

We have to prove that

Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ ifreg (ν = ν) e_{1}[ν/r] e_{2}[ν/r]

This implies that we have to prove that

Ψ; Δ, ν; Θ; Φ[ν/r]; Γ[ν/r] ⊢ e_{1}[ν/r]

But we already know this.

Lemma D.6 If Θ, t:κ′ ⊢ τ : κ and Θ ⊢ τ′ : κ′, then Θ ⊢ τ[τ′/t] : κ

Proof The proof is a straightforward induction over the structure of τ.

Lemma D.7 If Δ; Θ, t:κ; Φ ⊢ σ and Θ ⊢ τ : κ, then Δ; Θ; Φ ⊢ σ[τ/t]

Proof The proof is again a straighforward induction over the structure of σ.

Lemma D.8 If Ψ; Δ; Θ, t:κ; Φ; Γ ⊢ op : σ and Θ ⊢ τ : κ then Ψ; Δ; Θ; Φ; Γ[τ/t] ⊢ op[τ/t] : σ[τ/t]

Proof The proof is by induction over the derivation for op.

Lemma D.9 If Ψ; Δ; Θ, t:κ; Φ; Γ ⊢ e and · ⊢ τ′ : κ then Ψ; Δ; Θ; Φ; Γ[τ′/t] ⊢ e[τ′/t]

Proof The proof is again by induction over the derivation for e.

Lemma D.10 If Δ; Θ; Φ, α:Δ′ ⊢ σ and Δ′; Θ; Φ ⊢ σ′, then Δ; Θ; Φ ⊢ σ[σ′/α]

Proof The proof is a straighforward induction over the structure of σ.

Lemma D.11 If Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ op : σ and Δ′; Θ; Φ ⊢ σ′ then Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ op[σ′/α] : σ[σ′/α]

Proof The proof is again by induction over the typing derivation for op. We will consider only the case for region packages. case ⟨r ∈ Δ′ = ρ, v⟩: We have that

Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ ⟨r ∈ Δ′ = ρ, v⟩ : ∃r ∈Δ′.(σ atr) and Δ′; Θ; Φ ⊢ σ′. This implies that Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ v : σ[ρ/r] atρ and ρ ∈ Δ′ and Δ′ ⊂ Δ. Applying the inductive hypothesis we get that

Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ v[σ′/α] : (σ[ρ/r])[σ′/α] atρ

Since r does not occur in Δ, and Δ′ ⊂ Δ, therefore r does not occur free in σ′. Therefore we have that

Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ v[σ′/α] : (σ[σ′/α])[ρ/r] atρ

This leads to the lemma.

Lemma D.12 If Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ e and Δ′; Θ; Φ ⊢ σ′ then

Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ e[σ′/α]

Proof The proof is by induction over the derivation of e.

case open v as ⟨r, x⟩ ine: We have that

Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ v : ∃r ∈Δ_{1}.(σ atr)

and Ψ; Δ, r; Θ; Φ, α: Δ′; Γ, x: σ at r ⊢ e. Applying lemma D.11 to the derivation for v we get that

Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ v[σ′/α] : ∃r ∈Δ_{1}.(σ[σ′/α] atr)

Applying the inductive hypothesis to the derivation for e we get that

Ψ; Δ, r; Θ; Φ; Γ[σ′/α], x:σ[σ′/α] atr ⊢ e[σ′/α]

This leads to the required result.

case ifreg (r_{1} = r_{2}) e_{1} e_{2}: We have that

Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ e_{2} and

Ψ; Δ[r, r/r_{1}, r_{1}]; Θ;
Φ[r, r/r_{1}, r_{1}], α:Δ′[r, r/r_{1}, r_{1}]; Γ[r, r/r_{1}, r_{2}] ⊢
e_{1}[r, r/r_{1}, r_{2}]

Applying the inductive hypothesis to the derivation of e_{2} leads to

Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ e_{2}[σ′/α]

By lemma D.1 we have that

Δ′[r, r/r_{1}, r_{2}]; Θ; Φ[r, r/r_{1}, r_{2}] ⊢ σ′[r, r/r_{1}, r_{2}]

Substitute σ′[r, r/r_{1}, r_{2}] in the derivation for e_{1} and by applying the inductive hypothesis we get that

\begin{matrix}Ψ; Δ[r, r/r_{1}, r_{1}]; Θ; Φ[r, r/r_{1}, r_{1}]; (Γ[σ′/α])[r, r/r_{1}, r_{2}] ⊢ \\ (e_{1}[σ′/α])[r, r/r_{1}, r_{2}] \end{matrix}

This leads to the required result.

case ifreg (r = ν) e_{1} e_{2}: We have that

Ψ; Δ; Θ; Φ, α:Δ′; Γ ⊢ e_{2} and

Ψ; Δ[ν/r]; Θ; Φ[ν/r], α:Δ′[ν/r]; Γ[ν/r] ⊢ e_{1}[ν/r]

Applying the inductive hypothesis to the derivation of e_{2} leads to

Ψ; Δ; Θ; Φ; Γ[σ′/α] ⊢ e_{2}[σ′/α]

By lemma D.1 we have that

Δ′[ν/r]; Θ; Φ[ν/r] ⊢ σ′[ν/r]

Substituting σ′[ν/r] in the derivation for e_{1} and applying the inductive hypothesis gives us that

Ψ; Δ[ν/r]; Θ; Φ[ν/r]; (Γ[σ′/α])[ν/r] ⊢ (e_{1}[σ′/α])[ν/r]

which leads to the required result.

Lemma D.13 If Ψ; Δ; Θ; Φ; Γ, x:σ′ ⊢ op : σ and

Ψ; Δ; Θ; Φ; Γ ⊢ v′ : σ′ then Ψ; Δ; Θ; Φ; Γ ⊢ op[v′/x] : σ Proof The proof is by induction over the typing derivation for op. The new cases follow in a straightforward way.

Lemma D.14 If Ψ; Δ; Θ; Φ; Γ ⊢ v : σ and Δ_{1}; Θ; Φ|_{Δ_{1}} ⊢ σ and Δ_{1} ⊂ Δ, then Ψ|_{Δ_{1}}; Δ_{1}; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}} ⊢ v : σ

Proof The proof is by induction over the derivation for v. We will show only the extra case here. case ⟨r ∈ Δ_{2} = ρ, v⟩: We have that Ψ; Δ; Θ; Φ; Γ ⊢ ⟨r ∈ Δ_{2} = ρ, v⟩ : ∃r ∈Δ_{2}.(σ atr). This implies that Ψ; Δ; Θ; Φ; Γ ⊢ v : σ[ρ/r] atρ and ρ ∈ Δ_{2} and Δ_{2} ⊂ Δ. We also have that Δ_{1}; Θ; Φ|_{Δ_{1}} ⊢ ∃r ∈Δ_{2}.(σ atr). This implies that Δ_{2} ⊂ Δ_{1}. Moreover, Δ_{1}, r; Θ; Φ|_{Δ_{1}} ⊢ σ. By lemma D.1 we get that Δ_{1}, ρ; Θ; (Φ|_{Δ_{1}})[ρ/r] ⊢ σ[ρ/r]. But since ρ ∈ Δ_{1} and r does not occur free in Φ|_{Δ_{1}}, we get that Δ_{1}; Θ; Φ|_{Δ_{1}} ⊢ σ[ρ/r]. Applying the inductive hypothesis to the derivation for v we get that Ψ|_{Δ_{1}}; Δ_{1}; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}} ⊢ v : σ[ρ/r] atρ. This implies that Ψ|_{Δ_{1}}; Δ_{1}; Θ; Φ|_{Δ_{1}}; Γ|_{Δ_{1}} ⊢ ⟨r ∈ Δ_{2} = ρ, v⟩ : ∃r ∈Δ_{2}.(σ atr)

Lemma D.15 If Ψ; Δ; Θ; Φ; Γ, x:σ ⊢ e and Ψ; Δ; Θ; Φ; Γ ⊢ v : σ then Ψ; Δ; Θ; Φ; Γ ⊢ e[v/x]

Proof The proof is by induction over the derivation of e. We will only consider the case for ifreg. case ifreg (r = ν) e_{1} e_{2}: By definition we have that

Ψ; Δ[ν/r]; Θ; Φ[ν/r]; Γ[ν/r], x:σ[ν/r] ⊢ e_{1}[ν/r]

and Ψ; Δ; Θ; Φ; Γ, x: σ ⊢ e_{2}. Applying the inductive hypothesis to the derivation of e_{2}, we get that Ψ; Δ; Θ; Φ; Γ ⊢ e_{2}[v/x]. By lemma D.4 we know that

Ψ; Δ[ν/r]; Θ; Φ[ν/r]; Γ[ν/r] ⊢ v[ν/r] : σ[ν/r]

Substituting v[ν/r] for x in the derivation for e_{1} leads to the lemma. case ifreg (r_{1} = r_{2}) e_{1} e_{2}: By definition we have that

Ψ; Δ[r, r/r_{1}, r_{2}]; Θ;
Φ[r, r/r_{1}, r_{2}]; Γ[r, r/r_{1}, r_{2}], x:σ[r, r/r_{1}, r_{2}] ⊢
e_{1}[r, r/r_{1}, r_{2}]

and Ψ; Δ; Θ; Φ; Γ, x:σ ⊢ e_{2}. By lemma D.4 we know that

\begin{matrix}Ψ; Δ[r, r/r_{1}, r_{2}]; Θ; Φ[r, r/r_{1}, r_{2}]; Γ[r, r/r_{1}, r_{2}] ⊢ \\ v[r, r/r_{1}, r_{2}] : σ[r, r/r_{1}, r_{2}] \end{matrix}

Substituting v[r, r/r_{1}, r_{2}] and v in the derivation of e_{1} and e_{2} respectively, and applying the inductive hypothesis leads to the lemma.

Proposition D.16 (Type Preservation) If ⊢ (M, e) and (M, e) ⟹ (M′, e′) then ⊢ (M′, e′). Proof The proof is by induction over the evaluation relation. We will consider only the additional cases here. The lemma follows in a straightforward way for the ifreg cases. case open ⟨r ∈ Δ = ν, v⟩ as ⟨r, x⟩ ine: We know that

Ψ; Dom(Ψ); ·; ·; · ⊢ open ⟨r ∈ Δ = ν, v⟩ as ⟨r, x⟩ ine

This implies that

Ψ; Dom(Ψ); ·; ·; · ⊢ ⟨r ∈ Δ = ν, v⟩ : ∃r ∈Δ.(σ atr)

where Δ ⊂ Dom(Ψ). By the typing rule for region packages, we have that ν ∈ Dom(Ψ) and that Ψ; Dom(Ψ); ·; ·; · ⊢ v : σ[ν/r] atν. We also have that Ψ; Dom(Ψ), r; ·; ·; x:σ atr ⊢ e. By lemma D.5 and since ν ∈ Dom(Ψ) we get that

Ψ; Dom(Ψ); ·; ·; x:σ[ν/r] atν ⊢ e[ν/r]

Applying lemma D.15 leads to the result.

Lemma D.17 (Canonical forms)

1. If Ψ; Δ; ·; ·; · ⊢ v : intthen v = n.

2. If Ψ; Δ; ·; ·; · ⊢ v : σ atν then v = ν.ℓ.

3. If Ψ; Δ; ·; ·; · ⊢ v : σ_{1} × σ_{2} then v = (v_{1}, v_{2}).

4. If Ψ; Δ; ·; ·; · ⊢ v : ∃t:κ.σ then v = ⟨t=τ, v′:σ⟩.

5. If Ψ; Δ; ·; ·; · ⊢ v : ∃α:Δ′.σ then v = ⟨α:Δ′ =σ_{1}, v′:σ_{2}⟩.

6. If Ψ; Δ; ·; ·; · ⊢ v : ∃r ∈Δ′.(σ atr) then

v = ⟨r ∈ Δ′ = ρ, v′⟩.

7. If Ψ; Δ; ·; ·; · ⊢ v : ∀⟦τ⃗⟧[r⃗](σ⃗) ⟶^{ρ} 0 then v = v′⟦τ⃗⟧.

8. If Ψ; Δ; ·; ·; · ⊢ v : ∀[t⃗:κ][r⃗](σ⃗) → 0

then v = λ[t⃗:κ][r⃗](x⃗:σ).e.

Proof The proof follows from the inspection of the typing rules for values.

Proposition D.18 (Progress) If ⊢ (M, e) then either e = haltv or there exists a (M′, e′) such that (M, e) ⟹ (M′, e′). Proof The proof is by induction over the structure of e. The ifreg cases follow in a straightforward way. We will consider only the region open construct. case open v as ⟨r, x⟩ ine: We know that

Ψ; Dom(Ψ); ·; ·; · ⊢ open v as ⟨r, x⟩ ine

This means that

Ψ; Dom(Ψ); ·; ·; · ⊢ v : ∃r ∈Δ.(σ atr)

By lemma D.17 we get that v = ⟨r ∈ Δ = ρ, v′⟩. By the typing rule for region packages, we get that ρ ∈ Dom(Ψ). This means that ρ = ν for some ν. Therefore, we have that

Ψ; Dom(Ψ); ·; ·; · ⊢ open ⟨r ∈ Δ = ν, v′⟩ as ⟨r, x⟩ ine

But by the operational semantics this goes to (M, e[ν, v′/r, x]).