From System F to Typed Assembly Language ^{∗} (Extended Version)

Greg Morrisett David Walker Karl Crary Neal Glew

Cornell University

November 21, 1997

Abstract

We motivate the design of a statically typed assembly language (TAL) and present a typepreserving translation from System F to TAL. The TAL we present is based on a conventional RISC assembly language, but its static type system provides support for enforcing high-level language abstractions, such as closures, tuples, and objects, as well as user-defined abstract data types. The type system ensures that well-typed programs cannot violate these abstractions. In addition, the typing constructs place almost no restrictions on low-level optimizations such as register allocation, instruction selection, or instruction scheduling.

Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly language provide a fully automatic way to produce proof carrying code, suitable for use in systems where untrusted and potentially malicious code must be checked for safety before execution.

1 Introduction

Compiling a source language to a statically typed intermediate language has compelling advantages over a conventional untyped compiler. An optimizing compiler for a high-level language such as ML may make as many as 20 passes over a single program, performing sophisticated analyses and transformations such as CPS conversion [15, 35, 3, 13, 19], closure conversion [21, 40, 20, 4, 27], unboxing [23, 31, 39], subsumption elimination [10, 12], or region inference [8]. Many of these optimizations require type information in order to succeed, and even those that do not often benefit from the additional structure supplied by a typing discipline [23, 19, 31, 37]. Furthermore, the ability to typecheck intermediate code provides an invaluable tool for debugging new transformations and optimizations [41, 29].

Today a small number of compilers work with typed intermediate languages in order to realize some or all of these benefits [23, 34, 7, 41, 25, 38, 14]. However, in all of these compilers, there is a conceptual line where types are lost. For instance, the TIL/ML compiler preserves type information through approximately 80% of compilation, but the remaining 20% is untyped.

∗This material is based on work supported in part by AFOSR grant F49620-97-1-0013, ARPA/RADC grant FC30602-96-1-0317, NSF grant CCR-9244739, and ONR grant N00014-92-J-1764. Any opinions, findings, and conclusions or recommendations in this publication are those of the authors and do not reflect the views of these agencies.

We show how to eliminate the untyped portions of a compiler and by so doing, extend the approach of compiling with typed intermediate languages to typed target languages. The target language in this paper is a strongly typed assembly language (TAL) based on a generic RISC instruction set. The type system for the language is surprisingly standard, supporting tuples, polymorphism, existentials, and a very restricted form of function pointer, yet it is sufficiently powerful that we can automatically generate well-typed and efficient code from high-level ML-like languages. Furthermore, we claim that the type system does not seriously hinder low-level optimizations such as register allocation, instruction selection, instruction scheduling, and copy propagation.

TAL not only allows us to reap the benefits of types throughout a compiler, but it also enables a practical system for executing untrusted code both safely and efficiently. For example, as suggested by the SPIN project [6], operating systems could allow users to download TAL extensions into the kernel. The kernel could typecheck the TAL code to ensure that the code never accesses hidden resources within the kernel, always calls kernel routines with the right number and types of arguments, etc., and then assemble and dynamically link the code into the kernel.^{1} However, SPIN currently requires the user to write the extension in a single high-level language (Modula-3) and use a single trusted compiler (along with cryptographic signatures) in order to ensure the safety of the extension. In contrast, a kernel based on a typed assembly language could support extensions written in a variety of high-level languages using a variety of untrusted compilers, as the safety of the resulting assembly code can be checked independently of the source code or the compiler. Furthermore, critical inner-loops could be hand-written in assembly language in order to achieve optimal performance. TAL could also be used to support extensible web-browsers, extensible servers, active networks, or any other “kernel” where security, performance, and language independence are desired.

Software Fault Isolation (SFI) [47] also provides memory safety and language independence. However, SFI requires the insertion of extra “sandboxing” code, corresponding to dynamic type tests, to ensure that the extension is safe. In contrast, TAL does not have the overhead of the additional sandboxing code, as typechecking is performed offline.

With regard to these security properties, TAL is an instance of Necula and Lee’s proof carrying code (PCC) [33, 32]. Necula suggests that the relevant operational content of simple type systems may be encoded using extensions to first-order predicate logic, and proofs of relevant security properties such as memory safety may be automatically verified [32]. In addition, Necula’s approach places no restrictions on code sequences or instruction scheduling, whereas TAL has a small number of such restrictions (see Section 6.2). However, in general there is no complete algorithm for constructing the proof that the code satisfies the desired security properties. In contrast, we provide a fully automatic procedure for generating typed assembly language from a well-formed source term.

1Of course, while type safety implies many important security properties such as memory safety, there are a variety of other important security properties, such as termination, that do not follow from type safety.

1.1 Overview

In order to motivate the typing constructs in TAL and to justify our claims about its expressiveness, we spend much of this paper sketching a compiler from a variant of the polymorphic λ-calculus to TAL. The eager reader may wish to glance at Figure 26 for a sample TAL program.

Our compiler is structured as five translations between six typed calculi:

[figure: λ^{F}; CPS-conversion; λ^{K}; Closure conversion; λ^{C}; Hoisting; λ^{H}; Allocation; λ^{A}; Code generation; TAL]

Each of these calculi is used as a first-class programming calculus in the sense that each translation accepts any well-typed program of its input calculus; it does not assume that the input is the output from the preceding translation. This allows the compiler to aggressively optimize code between any of the translation steps. The inspiration for the phases and their ordering is derived from SML/NJ [5, 3] (which is in turn based on the Rabbit [40] and Orbit compilers [20]) except that types are used throughout compilation.

The rest of this paper proceeds by describing each of the languages and translations in our compiler in full detail. We give the syntax and static semantics of each language as well as type-directed and type-preserving translations between them. Section 2 presents λ^{F}, the compiler’s source language. Section 3 presents the first intermediate language, λ^{K}, and gives a typed CPS translation to it based on Danvy and Filinski [13] and Harper and Lillibridge [19]. Section 4 presents the next intermediate language, λ^{C}, and gives a typed closure translation based on, but considerably simpler than, the presentation of Minamide, Morrisett, and Harper [27]. Section 5 presents the λ^{A} intermediate language and a translation that makes allocation and initialization of data structures explicit. At this point in compilation, the intermediate code is essentially in a λ-calculus syntax for assembly language, following the ideas of Wand [48]. Finally, Section 6 presents our typed assembly language and defines a translation from λ^{A} to TAL. In Section 7 we show the type correctness of the compiler and in Section 8 we discuss extensions to TAL to support language constructs not considered here.

2 System F

The source language for our compiler, λ^{F}, is a call-by-value variant of System F [16, 17, 36] (the polymorphic λ-calculus) augmented with products and recursion on terms. The syntax for λ^{F} appears below:

types  τ ::= α | int | τ_{1} → τ_{2} | ∀α.τ | ⟨τ_{1}, …, τ_{n}⟩
terms  e ::= x | i | fix x(x_{1}:τ_{1}):τ_{2}.e | e_{1}e_{2} | Λα.e | e[τ] |
⟨e_{1}, …, e_{n}⟩ | π_{i}(e) | e_{1} p e_{2} | if0 (e_{1}, e_{2}, e_{3})
primitives  p ::= + | − | ×
type contexts  Δ ::= α_{1}, …, α_{n}
value contexts  Γ ::= x_{1}:τ_{1}, …, x_{n}:τ_{n}

In order to simplify the presentation, λ^{F} has only integers as a base type (ranged over by the metavariable i). We use X⃗ to denote a vector of syntactic objects drawn from X. For instance,

{FTV (τ) ⊆ Δ \atop Δ ⊢_{F} τ}

Δ; Γ ⊢_{F} x : τ (Γ(x) = τ)  Δ; Γ ⊢_{F} i : int
Δ ⊢_{F} τ_{1} Δ ⊢_{F} τ_{2} Δ; Γ{x:τ_{1} → τ_{2}, x_{1}:τ_{1}} ⊢_{F} e : τ_{2}

Δ; Γ ⊢_{F} fix x(x_{1}:τ_{1}):τ_{2}.e : τ_{1} → τ_{2} (x, x_{1} ∉ Γ)

Δ; Γ ⊢_{F} e_{1} : τ_{1} → τ_{2} Δ; Γ ⊢_{F} e_{2} : τ_{1}
Δ; Γ ⊢_{F} e_{1}e_{2} : τ_{2}
{Δ\{α\}; Γ ⊢_{F} e : τ \atop Δ; Γ ⊢_{F} Λα.e : ∀α.τ} (α ∉ Δ)

Δ ⊢_{F} τ Δ; Γ ⊢_{F} e : ∀α.τ′

Δ; Γ ⊢_{F} e[τ] : τ′[τ/α]

{Δ; Γ ⊢_{F} e_{i} : τ_{i} \atop Δ; Γ ⊢_{F} ⟨e_{1}, …, e_{n}⟩ : ⟨τ_{1}, …, τ_{n}⟩}  {Δ; Γ ⊢_{F} e : ⟨τ_{1}, …, τ_{n}⟩ \atop Δ; Γ ⊢_{F} π_{i}(e) : τ_{i}} (1 ≤ i ≤ n)
Δ; Γ ⊢_{F} e_{1} : int Δ; Γ ⊢_{F} e_{2} : int
Δ; Γ ⊢_{F} e_{1} p e_{2} : int

Δ; Γ ⊢_{F} e_{1} : int Δ; Γ ⊢_{F} e_{2} : τ Δ; Γ ⊢_{F} e_{3} : τ

Δ; Γ ⊢_{F} if0 (e_{1}, e_{2}, e_{3}) : τ

Figure 1: Static Semantics of λ^{F}

⟨τ⃗⟩ is shorthand for a product type ⟨τ_{1}, …, τ_{n}⟩. The term fix x(x_{1}:τ_{1}):τ_{2}.e represents a recursivelydefined function x with argument x_{1} of type τ_{1} and body e. Hence, both x and x_{1} are bound within e. Similarly, α is bound in e for Λα.e and bound in τ for ∀α.τ. As usual, we consider syntactic objects to be equivalent up to alpha-conversion of bound variables.

We interpret λ^{F} with a conventional call-by-value operational semantics (not presented here). The static semantics (given in Figure 1) is specified as a set of inference rules for concluding judgments of the form Δ; Γ ⊢_{F} e : τ where Δ is a context containing the free type variables of Γ, e, and τ; Γ is a context that assigns types to the free variables of e; and τ is the type of e. A judgment Δ ⊢_{F} τ asserts that type τ is well-formed under type context Δ.

As a running example, we will consider the compilation of the following computation of 6 factorial:

(fix f(n:int):int.if0 (n, 1, n × f(n − 1))) 6.

3 CPS Conversion

The first compilation stage is conversion to continuation-passing style (CPS). This stage names all intermediate computations and eliminates the need for a control stack. All unconditional control transfers, including function invocation and return, are achieved via function call. The target calculus for this phase is λ^{K}:

types  τ ::= α | int | ∀[α⃗].(τ⃗) → void | ⟨τ⃗⟩
terms  e ::= v[τ⃗](v⃗) | if0 (v, e_{1}, e_{2}) | halt[τ]v | let x = v in e |
let x = π_{i}(v) in e | let x = v_{1} p v_{2} in e
values  v ::= x | i | ⟨v⃗⟩ | fix x[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e
primitives  p ::= + | − | ×
type contexts  Δ ::= α_{1}, …, α_{n}
value contexts  Γ ::= x_{1}:τ_{1}, …, x_{n}:τ_{n}

Code in λ^{K} is nearly linear: it consists of a series of let bindings followed by a function call. The exception to this is the if0 construct, which is still a tree containing two expressions.

In λ^{K} there is only one abstraction mechanism (fix), which abstracts both type and value variables, thereby simplifying the rest of the compiler. The corresponding ∀ and → types are also combined. However, we abbreviate ∀[ ].(τ⃗) → void as (τ⃗) → void.

Unlike in λ^{F}, functions in λ^{K} do not return values; instead, they invoke continuations. The function notation “→ void” is intended to suggest this fact. Execution is completed by the construct halt[τ]v, which accepts a result value v of type τ and terminates the computation. Typically, this construct is used by the top-level continuation. Since expressions never return values, typing judgments for expressions do not state types. Instead, the judgment Δ; Γ ⊢_{K} e indicates that the expression e is well-formed under type and value contexts Δ and Γ. Aside from these issues, the static semantics for λ^{K} is completely standard and appears in Figure 2.

3.1 Translating λ^{F} to λ^{K}

The implementation of CPS-conversion follows Danvy and Filinski [13] and Harper and Lillibridge [19]. Danvy and Filinski give a CPS translation with a two-level type system that distinguishes between static (or “administrative”) β-redices and dynamic ones. They use this in a onepass translation that produces an efficient CPS value and prove the resulting value βη-equivalent to a standard CPS translation (as given by Fischer and Plotkin [15, 35]) They also show how to modify their translation so that it is “properly tail-recursive” (i.e., so that the unnecessary η-expansions of tail-recursive functions are eliminated). Our translation uses both the two-level system and the tail-recursion optimizations. Harper and Lillibridge discuss the typing properties of CPS conversion of F_{ω} augmented with callcc and abort primitives. We used their call-by-value translation to guide our translation. Note that a real implementation would uncurry a type abstraction followed by a value abstraction during the translation, creating a single polymorphic function.

The type translation K[[ · ]] mapping λ^{F} types to λ^{K} types is given in Figure 3. For any λ^{F} type τ, N [[τ]] represents the λ^{K} type for a τ-continuation, which is (K[[τ]]) → void. The translation of terms (Figures 4 and 5) is given by three judgments. Full programs are translated by the judgment ⊢_{F} e_{F} : τ ⇝^{cps} e_{cps}, which asserts that e_{cps} is a correct CPS conversion of the program e_{F}. Most of the work is done by two other judgments: one for terms in tailcall positions and another for all other positions.

The non-tailcall translation is given by the judgment Δ; Γ ⊢_{F} e_{F} : τ ⇝^{cps^{∗}} e_{cps}. The result, e_{cps}, is a static function that takes a static continuation representing the rest of the program and invokes it

{FTV (τ) ⊆ Δ \atop Δ ⊢_{K} τ}

Δ; Γ ⊢_{K} x : τ (Γ(x) = τ)  Δ; Γ ⊢_{K} i : int

{Δ; Γ ⊢_{K} v_{i} : τ_{i} \atop Δ; Γ ⊢_{K} ⟨v_{1}, …, v_{n}⟩ : ⟨τ_{1}, …, τ_{n}⟩}

Δ{α⃗} ⊢_{K} τ_{i} Δ{α⃗}; Γ{x:∀[α⃗](τ⃗) → void, x_{1}:τ_{1}, …, x_{n}:τ_{n}} ⊢_{K} e

Δ; Γ ⊢_{K} fix x[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e : ∀[α⃗](τ⃗) → void (x, x_{i} ∉ Γ, α_{i} ∉ Δ)

Δ ⊢_{K} σ_{i} Δ; Γ ⊢_{K} v : ∀[α_{1}, …, α_{n}].(τ_{1}, …, τ_{m}) → void Δ; Γ ⊢_{K} v_{j} : τ_{j}[σ⃗/α⃗]
Δ; Γ ⊢_{K} v[σ_{1}, …, σ_{n}](v_{1}, …, v_{m})
Δ; Γ ⊢_{K} v : int Δ; Γ ⊢_{K} e_{1} Δ; Γ ⊢_{K} e_{2}

Δ; Γ ⊢_{K} if0 (v, e_{1}, e_{2})

Δ; Γ ⊢_{K} v : τ
Δ; Γ ⊢_{K} halt[τ]v
Δ; Γ ⊢_{K} v : τ Δ; Γ{x:τ} ⊢_{K} e
Δ; Γ ⊢_{K} let x = v in e

(x ∉ Γ)
Δ; Γ ⊢_{K} v : ⟨τ_{1}, …, τ_{n}⟩ Δ; Γ{x:τ_{i}} ⊢_{K} e

Δ; Γ ⊢_{K} let x = π_{i}(v) in e

(x ∉ Γ, 1 ≤ i ≤ n)
Δ; Γ ⊢_{K} v_{1} : int Δ; Γ ⊢_{K} v_{2} : int Δ; Γ{x:int} ⊢_{K} e

Δ; Γ ⊢_{K} let x = v_{1} p v_{2} in e

(x ∉ Γ)

Figure 2: Static Semantics of λ^{K}

K[[α]] =^{def} α
K[[int]] =^{def} int
K[[τ_{1} → τ_{2}]] =^{def} (K[[τ_{1}]], N [[τ_{2}]]) → void
K[[∀α.τ]] =^{def} ∀[α].(N [[τ]]) → void
K[[⟨τ_{1}, …, τ_{n}⟩]] =^{def} ⟨K[[τ_{1}]], …, K[[τ_{n}]]⟩
N [[τ]] =^{def} (K[[τ]]) → void

Figure 3: Type Translation from λ^{F} to λ^{K}

∅; ∅ ⊢_{F} e : τ ⇝^{cps^{∗}} e′

⊢_{F} e : τ ⇝^{cps} e′@(λy.halt[K[[τ]]]y)

Δ; Γ ⊢_{F} x : τ ⇝^{cps^{∗}} λk.k@x (Γ(x) = τ)  Δ; Γ ⊢_{F} i : int ⇝^{cps^{∗}} λk.k@i
Δ ⊢_{F} τ_{1} Δ ⊢_{F} τ_{2} Δ; Γ{x:τ_{1} → τ_{2}, x_{1}:τ_{1}} ⊢_{F} e : τ_{2} ⇝^{cps^{t}} e′

Δ; Γ ⊢_{F} fix x(x_{1}:τ_{1}):τ_{2}.e : τ_{1} → τ_{2} ⇝^{cps^{∗}} λk.k@(fix x[ ](x_{1}:K[[τ_{1}]], c:N [[τ_{2}]]).e′@c)

(x, x_{1} ∉ Γ)

Δ; Γ ⊢_{F} e_{1} : τ_{1} → τ_{2} ⇝^{cps^{∗}} e′_{1} Δ; Γ ⊢_{F} e_{2} : τ_{1} ⇝^{cps^{∗}} e′_{2}

Δ; Γ ⊢_{F} e_{1}e_{2} : τ_{2} ⇝^{cps^{∗}} λk.e′_{1}@(λy_{1}.e′_{2}@(λy_{2}.y_{1}[ ](y_{2}, fix [ ](z:K[[τ_{2}]]).k@z)))

Δ{α}; Γ ⊢_{F} e : τ ⇝^{cps^{t}} e′

Δ; Γ ⊢_{F} Λα.e : ∀α.τ ⇝^{cps^{∗}} λk.k@(fix [α](c:N [[τ]]).e′@c)

(α ∉ Δ)
Δ ⊢_{F} τ Δ; Γ ⊢_{F} e : ∀α.τ′ ⇝^{cps^{∗}} e′

Δ; Γ ⊢_{F} e[τ] : τ′[τ/α] ⇝^{cps^{∗}} λk.e′@(λy.y[K[[τ]]](fix [ ](z:K[[τ′[τ/α]]]).k@z))

Δ; Γ ⊢_{F} e_{i} : τ_{i} ⇝^{cps^{∗}} e′_{i}

\begin{matrix}Δ; Γ ⊢_{F} ⟨e_{1}, …, e_{n}⟩ : ⟨τ_{1}, …, τ_{n}⟩ ⇝^{cps^{∗}} \\ λk.e′_{1}@(λy_{1}.e′_{2}@ ⋯ e′_{n}@(λy_{n}.k@⟨y_{1}, …, y_{n}⟩) ⋯) \end{matrix}

Δ; Γ ⊢_{F} e : ⟨τ_{1}, …, τ_{n}⟩⟩ ⇝^{cps^{∗}} e′

Δ; Γ ⊢_{F} π_{i}(e) : τ_{i} ⇝^{cps^{∗}} λk.e′@(λy.let z = π_{i}(y) in k@z)

(1 ≤ i ≤ n)

Δ; Γ ⊢_{F} e_{1} : int ⇝^{cps^{∗}} e′_{1} Δ; Γ ⊢_{F} e_{2} : int ⇝^{cps^{∗}} e′_{2}

Δ; Γ ⊢_{F} e_{1} p e_{2} : int ⇝^{cps^{∗}} λk.e′_{1}@(λy_{1}.e′_{2}@(λy_{2}.let z = y_{1} p y_{2} in k@z))

Δ; Γ ⊢_{F} e_{1} : int ⇝^{cps^{∗}} e′_{1} Δ; Γ ⊢_{F} e_{2} : τ ⇝^{cps^{t}} e′_{2} Δ; Γ ⊢_{F} e_{3} : τ ⇝^{cps^{t}} e′_{3}

Δ; Γ ⊢_{F} if0 (e_{1}, e_{2}, e_{3}) : τ ⇝^{cps^{∗}}

λk.e′_{1}@(λy.let c = fix [ ](z : K[[τ]]).k@z in

if0 (y, e′_{2}@c, e′_{3}@c))

Figure 4: Term Translation from λ^{F} to λ^{K} (except tailcalls)

Δ; Γ ⊢_{F} x : τ ⇝^{cps^{t}} λc.c[ ](x) (Γ(x) = τ)  Δ; Γ ⊢_{F} i : int ⇝^{cps^{t}} λc.c[ ](i)
Δ ⊢_{F} τ_{1} Δ ⊢_{F} τ_{2} Δ; Γ{x:τ_{1} → τ_{2}, x_{1}:τ_{1}} ⊢_{F} e : τ_{2} ⇝^{cps^{t}} e′

Δ; Γ ⊢_{F} fix x(x_{1}:τ_{1}):τ_{2}.e : τ_{1} → τ_{2} ⇝^{cps^{t}} λc.c[ ](fix x[ ](x_{1}:K[[τ_{1}]], c′:N [[τ_{2}]]).e′@c′)

(x, x_{1} ∉ Γ)
Δ; Γ ⊢_{F} e_{1} : τ_{1} → τ_{2} ⇝^{cps^{∗}} e′_{1} Δ; Γ ⊢_{F} e_{2} : τ_{1} ⇝^{cps^{∗}} e′_{2}

Δ; Γ ⊢_{F} e_{1}e_{2} : τ_{2} ⇝^{cps^{t}} λc.e′_{1}@(λy_{1}.e′_{2}@(λy_{2}.y_{1}[ ](y_{2}, c)))

Δ{α}; Γ ⊢_{F} e : τ ⇝^{cps^{t}} e′

Δ; Γ ⊢_{F} Λα.e : ∀α.τ ⇝^{cps^{t}} λc.c[ ](fix [α](c:N [[τ]]).e′@c)

(α ∉ Δ)
Δ ⊢_{F} τ Δ; Γ ⊢_{F} e : ∀α.τ′ ⇝^{cps^{∗}} e′

Δ; Γ ⊢_{F} e[τ] : τ′[τ/α] ⇝^{cps^{t}} λc.e′@(λy.y[K[[τ]]](c))

Δ; Γ ⊢_{F} e_{i} : τ_{i} ⇝^{cps^{∗}} e′_{i}

\begin{matrix}Δ; Γ ⊢_{F} ⟨e_{1}, …, e_{n}⟩ : ⟨τ_{1}, …, τ_{n}⟩ ⇝^{cps^{t}} \\ λc.e′_{1}@(λy_{1}.e′_{2}@ ⋯ e′_{n}@(λy_{n}.c[ ](⟨y_{1}, …, y_{n}⟩)) ⋯) \end{matrix}

Δ; Γ ⊢_{F} e : ⟨τ_{1}, …, τ_{n}⟩⟩ ⇝^{cps^{∗}} e′

Δ; Γ ⊢_{F} π_{i}(e) : τ_{i} ⇝^{cps^{t}} λc.e′@(λy.let z = π_{i}(y) in c[ ](z))

(1 ≤ i ≤ n)

Δ; Γ ⊢_{F} e_{1} : int ⇝^{cps^{∗}} e′_{1} Δ; Γ ⊢_{F} e_{2} : int ⇝^{cps^{∗}} e′_{2}

Δ; Γ ⊢_{F} e_{1} p e_{2} : int ⇝^{cps^{t}} λc.e′_{1}@(λy_{1}.e′_{2}@(λy_{2}.let z = y_{1} p y_{2} in c[ ](z)))

Δ; Γ ⊢_{F} e_{1} : int ⇝^{cps^{∗}} e′_{1} Δ; Γ ⊢_{F} e_{2} : τ ⇝^{cps^{t}} e′_{2} Δ; Γ ⊢_{F} e_{3} : τ ⇝^{cps^{t}} e′_{3}

Δ; Γ ⊢_{F} if0 (e_{1}, e_{2}, e_{3}) : τ ⇝^{cps^{t}} λc.e′_{1}@(λy.if0 (y, e′_{2}@c, e′_{3}@c))

Figure 5: Tailcall Term Translation from λ^{F} to λ^{K} with the result of computing e_{F}. The tailcall translation is given by the judgment Δ; Γ ⊢_{F} e_{F} : τ ⇝^{cps^{t}} e_{cps}. Its result, e_{cps}, is similar except that it is a static function taking a dynamic continuation (that is, a continuation coded in λ^{K}).

Throughout the translation, static functions and applications are denoted by λx.e and e_{1}@e_{2}, and dynamic functions and applications are written in λ^{K} syntax. The static variables k, y and y_{i} and the dynamic variables c, c′ and z, which are used internally by the translation, are always assumed fresh. An underscore is used in place of unreferenced variables.

Lemma 3.1 ∅; ∅ ⊢_{F} e : τ if and only if there exists e′ such that ⊢_{F} e : τ ⇝^{cps} e′.

Lemma 3.2 (CPS Conversion Type Correctness) If ⊢_{F} e : τ ⇝^{cps} e′ then ∅; ∅ ⊢_{K} e′.

These lemmas and the others like it are proved by induction on the source derivations.

When applied to the factorial example, this translation yields the following λ^{K} term:

(fix f [ ] (n:int, k:(int) → void).

if0 (n, k[ ](1),

let x = n − 1 in

f[ ](x, fix [ ] (y:int). let z = n × y in k[ ](z))))

[ ] (6, fix [ ] (n:int). halt[int]n)

4 Simplified Polymorphic Closure Conversion

The second compilation stage is closure conversion, which separates program code from data. This is done in two steps. Most of the work is done in the first step, closure conversion proper, which rewrites all functions so that they are closed. In order to do this, any variables from the context that are used in the function must be taken as additional arguments. These additional arguments are collected in an environment, which is paired with the (now closed) code to make a closure. In the second step, hoisting, closed function code is lifted to the top of the program, achieving the desired separation between code and data. We begin with closure conversion proper; the hoisting step is considered in Section 4.1.

Our approach to typed closure conversion is based on that of Minamide et al. [27]: If two functions with the same type but different free variables (and therefore different environment types) were naively closure converted, the types of their closures would not be the same. To prevent this, closures are given existential types [28] where the type of the environment is held abstract.

However, we propose an approach to polymorphic closure conversion that is considerably simpler than that of Minamide et al. which requires both abstract kinds and translucent types. Both of these mechanisms arise because Minamide et al. desire a type-passing interpretation of polymorphism where types are constructed and passed to polymorphic functions at run-time. Under a

types  τ ::= α | int | ∀[α⃗].(τ⃗) → void | ⟨τ⃗⟩ | ∃α.τ
terms  e ::= v(v⃗) | if0 (v, e_{1}, e_{2}) | halt[τ]v | let x = v in e | let x = π_{i}(v) in e |

let x = v_{1} p v_{2} in e | let [α, x] = unpack v in e

values  v ::= x | i | ⟨v⃗⟩ | v[τ] | pack [τ, v] as ∃α.τ′ | fixcode x[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e
primitives  p ::= + | − | ×
type contexts  Δ ::= α_{1}, …, α_{n}
value contexts  Γ ::= x_{1}:τ_{1}, …, x_{n}:τ_{n}

Figure 6: Syntax of λ^{C}

type-passing interpretation, polymorphic instantiation cannot be treated via substitution, as this requires making a copy of the code at run-time. Instead, a closure is constructed that consists of closed code, a value environment mapping variables to values, and a type environment mapping type variables to types.

In our approach, we assume a type-erasure interpretation of polymorphism as in The Definition of Standard ML [26], and polymorphic instantiation is semantically handled via substitution (i.e., making a copy of the code with the types substituted for the type variables). As types will ultimately be erased from terms for execution, the “copies” can (and will) be represented by the same term. This avoids the need for abstract kinds (since there are no type environments), as well as translucent types. A type-erasure interpretation is not without its costs: It precludes some advanced implementation techniques [31, 43, 1, 30] and has subtle interactions with side-effects. We address the latter concern by forcing polymorphic abstractions to be values [42, 49] (i.e., they must be syntactically attached to value abstractions).

To support this interpretation, we consider the partial application of functions to type arguments to be values. For example, suppose v has the type ∀[α⃗, β⃗].(τ⃗) → void where the type variables α⃗ are intended for the type environment and the type variables β⃗ are intended for the function’s type arguments. If σ⃗ is a vector of types to be used for the type environment, then the partial instantiation v[σ⃗] is still treated as a value and has type ∀[β⃗].(τ⃗[σ⃗/α⃗]) → void. The syntax of λ^{C} is otherwise similar to λ^{K} and appears in Figure 6. The static semantics of λ^{C} appears in Figure 7. Notice in particular that the body e of a function expression fixcode x[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e must typecheck given only the type and value contexts α⃗ and {x:(τ_{1}, …, τ_{n}) → void, x_{1}:τ_{1}, …, x_{n}:τ_{n}}, which result from the fixcode abstraction. In other words, code must be closed.

The closure conversion algorithm is formalized as a type-directed translation in Figures 8 and 9. The translation of λ^{K} types is denoted by C[[ · ]]. Terms are translated by the judgment Δ; Γ ⊢_{K} e_{cps} ⇝^{clos} e_{clos}, which asserts that e_{clos} is a correct closure conversion of the term e_{cps}, and values are translated by the judgment Δ; Γ ⊢_{K} v_{cps} : τ ⇝^{clos} v_{clos}, which asserts that v_{clos} is a correct closure conversion of the value v_{cps}. The variables z, x_{code} and x_{env}, which are used internally by the translation, are always assumed fresh.

The key to the translation is the treatment of function types:

C[[∀[α⃗].(τ_{1}, …, τ_{n}) → void]] =^{def} ∃β.⟨∀[α⃗].(β, C[[τ_{1}]], …, C[[τ_{n}]]) → void, β⟩

The existentially-quantified variable β is the type of the value environment for the closure. The

{FTV (τ) ⊆ Δ \atop Δ ⊢_{C} τ}

Δ; Γ ⊢_{C} x : τ (Γ(x) = τ)  Δ; Γ ⊢_{C} i : int

{Δ; Γ ⊢_{C} v_{i} : τ_{i} \atop Δ; Γ ⊢_{C} ⟨v_{1}, …, v_{n}⟩ : ⟨τ_{1}, …, τ_{n}⟩}

Δ ⊢_{C} σ Δ; Γ ⊢_{C} v : ∀[α, β⃗].(τ⃗) → void

Δ; Γ ⊢_{C} v[σ] : ∀[β⃗].(τ⃗[σ/α]) → void

Δ ⊢_{C} τ Δ; Γ ⊢_{C} v : τ′[τ/α]

Δ; Γ ⊢_{C} pack [τ, v] as ∃α.τ′ : ∃α.τ′

α⃗ ⊢_{C} τ_{i} α⃗; {x:∀[α⃗].(τ⃗) → void, x_{1}:τ_{1}, …, x_{n}:τ_{n}} ⊢_{C} e

Δ; Γ ⊢_{C} fixcode x[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e : ∀[α⃗].(τ⃗) → void

Δ; Γ ⊢_{C} v : ∀[ ].(τ_{1}, …, τ_{n}) → void Δ; Γ ⊢_{C} v_{i} : τ_{i}
Δ; Γ ⊢_{C} v(v_{1}, …, v_{n})
Δ; Γ ⊢_{C} v : int Δ; Γ ⊢_{C} e_{1} Δ; Γ ⊢_{C} e_{2}
Δ; Γ ⊢_{C} if0 (v, e_{1}, e_{2})
Δ; Γ ⊢_{C} v : τ
Δ; Γ ⊢_{C} halt[τ]v
Δ; Γ ⊢_{C} v : τ Δ; Γ{x:τ} ⊢_{C} e
Δ; Γ ⊢_{C} let x = v in e

(x ∉ Γ)
Δ; Γ ⊢_{C} v : ⟨τ_{1}, …, τ_{n}⟩ Δ; Γ{x:τ_{i}} ⊢_{C} e

Δ; Γ ⊢_{C} let x = π_{i}(v) in e

(x ∉ Γ, 1 ≤ i ≤ n)
Δ; Γ ⊢_{C} v_{1} : int Δ; Γ ⊢_{C} v_{2} : int Δ; Γ{x:int} ⊢_{C} e

Δ; Γ ⊢_{C} let x = v_{1} p v_{2} in e

(x ∉ Γ)
Δ; Γ ⊢_{C} v : ∃α.τ Δα; Γ{x:τ} ⊢_{C} e

let [α, x] = unpack v in e

(x ∉ Γ, α ∉ Δ)

Figure 7: Static Semantics of λ^{C}

C[[α]] =^{def} α
C[[int]] =^{def} int
C[[∀[α⃗].(τ_{1}, …, τ_{n}) → void]] =^{def} ∃β.⟨∀[α⃗].(β, C[[τ_{1}]], …, C[[τ_{n}]]) → void, β⟩
C[[⟨τ_{1}, …, τ_{n}⟩]] =^{def} ⟨C[[τ_{1}]], …, C[[τ_{n}]]⟩

Figure 8: Type Translation from λ^{K} to λ^{C}

closure itself is a pair consisting of a piece of code that is instantiated with the type environment, and the value environment. The instantiated code takes as arguments the type arguments and value arguments of the original abstraction, as well as the value environment of the closure.

Lemma 4.1 ∅; ∅ ⊢_{K} e if and only if there exists e′ such that ∅; ∅ ⊢_{K} e ⇝^{clos} e′

Lemma 4.2 (Closure Conversion Type Correctness) If ∅; ∅ ⊢_{K} e ⇝^{clos} e′ then ∅; ∅ ⊢_{C} e′.

4.1 Hoisting

After closure conversion, all functions are closed and may be hoisted out to the top-level without difficulty. In a real compiler, these two phases would be combined but we have separated them here for simplicity. After hoisting, programs belong to a calculus, λ^{H}, that is similar to λ^{C} except that fixcode is no longer a value. Instead, code blocks are defined at the top-level by a letrec prefix, which is called a heap in anticipation of λ^{A} and TAL. A new value form, labels (ℓ), is used to refer to those code blocks. The syntax of λ^{H} appears in Figure 10.

These changes require a small change to the typing system. In addition to typing values, we also must assign heap types (ranged over by Ψ) to heaps. These heap types are added to value and term typing judgments as an additional context and are passed unmodified through each typing rule. There are also two new judgments: the judgment ⊢_{H} P indicates that the program P is well-formed, and the judgment Ψ ⊢_{H} b : ℓ ↦ τ indicates that the block b gives the label ℓ type τ assuming the heap has type Ψ. The static semantics of λ^{H} appear in Figure 11; rules that appear identically (except for the addition of heap types) in the static semantics of λ^{C} are omitted for brevity.

The translation of full programs from λ^{C} to λ^{H} is given by the judgment ⊢_{C} e_{clos} ⇝^{hst} e_{hst}, which states that e_{hst} is the hoisted version of the program e_{clos}. No translation is required for types. The translation rules are exactly as expected and are omitted in the interest of brevity.

Lemma 4.3 ∅; ∅ ⊢_{C} e if and only if there exists P such that ⊢_{C} e ⇝^{hst} P.

Lemma 4.4 (Hoisting Type Correctness) If ⊢_{C} e ⇝^{hst} P then ⊢_{H} P.

In Figure 12 appears the factorial example after the closure conversion and hoisting translations are applied and some simple optimizations are performed (beta reduction and copy propagation).

Δ ⊢_{K} τ_{i}  Γ = {y_{1}:τ′_{1}, …, y_{m}:τ′_{m}}  Δ = β⃗

Δα⃗; Γ[x:τ_{code}, x_{1}:τ_{1}, …, x_{n}:τ_{n}] ⊢_{K} e ⇝^{clos} e′

Δ; Γ ⊢_{K} fix x[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e : τ_{code} ⇝^{clos} pack [τ_{env}, ⟨v_{code}[β⃗], v_{env}⟩] as C[[τ_{code}]]

where τ_{code} = ∀[α⃗].(τ_{1}, …, τ_{n}) → void
τ_{env} = ⟨C[[τ′_{1}]], ⋯, C[[τ′_{m}]]⟩
v_{env} = ⟨y_{1}, …, y_{m}⟩
v_{code} = fixcode x_{code}[β⃗, α⃗](x_{env}:τ_{env}, x_{1}:C[[τ_{1}]], …, x_{n}:C[[τ_{n}]]).

let x = pack [τ_{env}, ⟨x_{code}[β⃗], x_{env}⟩] as C[[τ_{code}]] in let y_{1} = π_{1}(x_{env}) in

⋮

let y_{m} = π_{m}(x_{env}) in e′

(x, x_{i} ∉ Γ, α_{i} ∉ Δ)

Δ; Γ ⊢_{K} v : ∀[α_{1}, …, α_{m}].(τ_{1}, …, τ_{n}) → void ⇝^{clos} v′ Δ ⊢_{K} σ_{i} Δ; Γ ⊢_{K} v_{i} : τ_{i}[σ⃗/α⃗] ⇝^{clos} v′_{i}

Δ; Γ ⊢_{K} v[σ_{1}, …, σ_{m}](v_{1}, …, v_{n}) ⇝^{clos} e

where e = let [α_{env}, z] = unpack v′ in
let x_{code} = π_{1}(z) in
let x_{env} = π_{2}(z) in

x_{code}[C[[σ_{1}]]] ⋯ [C[[σ_{m}]]](x_{env}, v′_{1}, …, v′_{n})

Δ; Γ ⊢_{K} x : τ ⇝^{clos} x (Γ(x) = τ)  Δ; Γ ⊢_{K} i : int ⇝^{clos} i

Δ; Γ ⊢_{K} v_{i} : τ_{i} ⇝^{clos} v′_{i}

Δ; Γ ⊢_{K} ⟨v_{1}, …, v_{n}⟩ : ⟨τ_{1}, …, τ_{n}⟩ ⇝^{clos} ⟨v′_{1}, …, v′_{n}⟩

Δ; Γ ⊢_{K} v : int ⇝^{clos} v′ Δ; Γ ⊢_{K} e_{1} ⇝^{clos} e′_{1} Δ; Γ ⊢_{K} e_{2} ⇝^{clos} e′_{2}

Δ; Γ ⊢_{K} if0 (v, e_{1}, e_{2}) ⇝^{clos} if0 (v′, e′_{1}, e′_{2})

Δ; Γ ⊢_{K} v : τ ⇝^{clos} v′

Δ; Γ ⊢_{K} halt[τ]v ⇝^{clos} halt[C[[τ]]]v′
Δ; Γ ⊢_{K} v : τ ⇝^{clos} v′ Δ; Γ{x:τ} ⊢_{K} e ⇝^{clos} e′

Δ; Γ ⊢_{K} let x = v in e ⇝^{clos} let x = v′ in e′

(x ∉ Γ)
Δ; Γ ⊢_{K} v : ⟨τ_{1}, …, τ_{n}⟩ ⇝^{clos} v′ Δ; Γ{x:τ_{i}} ⊢_{K} e ⇝^{clos} e′
Δ; Γ ⊢_{K} let x = π_{i}(v) in e ⇝^{clos} let x = π_{i}(v′) in e′

(x ∉ Γ, 1 ≤ i ≤ n)
Δ; Γ ⊢_{K} v_{1} : int ⇝^{clos} v′_{1} Δ; Γ ⊢_{K} v_{2} : int ⇝^{clos} v′_{2} Δ; Γ{x:int} ⊢_{K} e ⇝^{clos} e′

Δ; Γ ⊢_{K} let x = v_{1} p v_{2} in e ⇝^{clos} let x = v′_{1} p v′_{2} in e′

(x ∉ Γ)

Figure 9: Term Translation from λ^{K} to λ^{C}

types  τ ::= α | int | ∀[α⃗].(τ⃗) → void | ⟨τ⃗⟩ | ∃α.τ
terms  e ::= v(v⃗) | if0 (v, e_{1}, e_{2}) | halt[τ]v | let x = v in e | let x = π_{i}(v) in e |

let x = v_{1} p v_{2} in e | let [α, x] = unpack v in e

values  v ::= x | ℓ | i | ⟨v⃗⟩ | v[τ] | pack [τ, v] as ∃α.τ′
blocks  b ::= ℓ ↦ code[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e
programs  P ::= letrec b⃗ in e
primitives  p ::= + | − | ×
type contexts  Δ ::= α_{1}, …, α_{n}
value contexts  Γ ::= x_{1}:τ_{1}, …, x_{n}:τ_{n}
heap types  Ψ ::= ℓ_{1}:τ_{1}, …, ℓ_{n}:τ_{n}

Figure 10: Syntax of λ^{H}

Ψ; Δ; Γ ⊢_{H} ℓ : τ (Ψ(ℓ) = τ)
α⃗ ⊢_{H} τ_{i} Ψ; α⃗; {x_{1}:τ_{1}, …, x_{n}:τ_{n}} ⊢_{H} e

Ψ ⊢_{H} ℓ ↦ code[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e : ℓ ↦ ∀[α⃗].(τ_{1}, …, τ_{n}) → void

∅ ⊢_{H} τ_{i} Ψ ⊢_{H} b_{i} : ℓ_{i} ↦ τ_{i} Ψ; ∅; ∅ ⊢_{H} e

⊢_{H} letrec b_{1}, …, b_{n} in e ( \begin{matrix}Ψ = ℓ_{1}:τ_{1}, …, ℓ_{n}:τ_{n} \\ ℓ_{j} ≠ ℓ_{k} when j ≠ k \end{matrix} )

Figure 11: New Rules in the Static Semantics of λ^{H} letrec ℓ_{fact} ↦ (* main factorial code block *)

code[ ](env:⟨⟩, n:int, k:τ_{k}).

if0 (n, (* true branch: continue with 1 *) let [β, k_{unpack}] = unpack k in let k_{code} = π_{0}(k_{unpack}) in let k_{env} = π_{1}(k_{unpack}) in

k_{code}(k_{env}, 1),

(* false branch: recurse with n − 1 *)

let x = n − 1 in

(* compute factorial of n − 1 and continue to k′ *) ℓ_{fact}(env, x, pack [⟨int, τ_{k}⟩, ⟨ℓ_{cont}, ⟨n, k⟩⟩] as τ_{k}))

ℓ_{cont} ↦ (* code block for continuation after factorial computation *)

code[ ](env:⟨int, τ_{k}⟩, y:int).

(* open the environment *) let n = π_{0}(env) in let k = π_{1}(env) in (* continue with n × y *) let z = n × y in let [β, k_{unpack}] = unpack k in let k_{code} = π_{0}(k_{unpack}) in let k_{env} = π_{1}(k_{unpack}) in

k_{code}(k_{env}, z)

ℓ_{halt} ↦ (* code block for top-level continuation *)

code[ ](env:⟨⟩, n:int). halt[int](n)

in ℓ_{fact}(⟨⟩, 6, pack [⟨⟩, ⟨ℓ_{halt}, ⟨⟩⟩] as τ_{k})

where τ_{k} is ∃α.⟨(α, int) → void, α⟩

Figure 12: Factorial in λ^{H}

types  τ ::= α | int | ∀[α⃗].(τ⃗) → void | ⟨τ_{1}^{φ_{1}}, …, τ_{n}^{φ_{n}}⟩ | ∃α.τ
initialization flags  φ ::= 0 | 1
terms  e ::= let d⃗ in v(v⃗) | let d⃗ in if0 (v, e_{1}, e_{2}) | let d⃗ in halt[τ]v
declarations  d ::= x = v | x = π_{i}(v) | x = v_{1} p v_{2} | [α, x] = unpack v |

x = malloc[τ⃗] | x = v[i] ← v′

values  v ::= x | ℓ | i | v[τ] | pack [τ, v] as ∃α.τ′
blocks  b ::= ℓ ↦ code[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e
programs  P ::= letrec b⃗ in e
primitives  p ::= + | − | ×
type contexts  Δ ::= α_{1}, …, α_{n}
value contexts  Γ ::= x_{1}:τ_{1}, …, x_{n}:τ_{n}
heap types  Ψ ::= ℓ_{1}:τ_{1}, …, ℓ_{n}:τ_{n}

Figure 13: Syntax of λ^{A}

5 Explicit Allocation

The λ^{H} intermediate language still has an atomic constructor for forming tuples, but machines must allocate space for a tuple and fill it out field by field; the allocation stage makes this process explicit. The syntax of λ^{A}, the target calculus of this stage, is similar to that of λ^{H}, and appears in Figure 13. Note that there is no longer a value form for tuples. The creation of an n-element tuple becomes a computation that is separated into an allocation step and n initialization steps. For example, if v_{0} and v_{1} are integers, the pair ⟨v_{0}, v_{1}⟩ is created as follows (where types have been added for clarity):

let x_{0}:⟨int^{0}, int^{0}⟩ = malloc[int, int]
x_{1}:⟨int^{1}, int^{0}⟩ = x_{0}[0] ← v_{0}
x :⟨int^{1}, int^{1}⟩ = x_{1}[1] ← v_{1}
⋮

The “x_{0} = malloc[int, int]” step allocates an uninitialized tuple and binds the address (i.e., label) of the tuple to x_{0}. The “0” superscripts on the types of the fields indicate that the fields are uninitialized, and hence no projection may be performed on those fields. The “x_{1} = x_{0}[0] ← v_{0}” step updates the first field of the tuple with the value v_{0} and binds the address of the tuple to x_{1}. Note that x_{1} is assigned a type where the first field has a “1” superscript, indicating that this field is initialized. Finally, the “x = x_{1}[1] ← v_{1}” step initializes the second field of the tuple with v_{1} and binds the address of the tuple to x, which is assigned the fully initialized type ⟨int^{1}, int^{1}⟩. Hence, both π_{0} and π_{1} are allowed on x.

Like all the intermediate languages of the compiler, this code sequence need not be atomic; it may be rearranged or optimized in any well-typed manner. The initialization flags on the types ensure that a field cannot be projected unless it has been initialized. Furthermore, the syntactic value restriction ensures there is no unsoundness in the presence of polymorphism. However, it is important to note that x[i] ← v is interpreted as an imperative operation, and thus at the end of the sequence, x_{0}, x_{1}, and x are all aliases for the same location, even though they have different (but compatible) types. Consequently, the initialization flags do not prevent a field from being initialized twice. It is possible to use monads [44, 22] or linear types [18, 45, 46] to ensure that a tuple is initialized exactly once, but we have avoided these approaches in the interest of a simpler type system.

The static semantics for λ^{A} are given in Figure 14. Figure 15 presents the type translation from λ^{H} to λ^{A}. All that happens is that initialization flags are added to each field of tuple types:

A[[⟨τ_{1}, …, τ_{n}⟩]] =^{def} ⟨A[[τ_{1}]]^{1}, …, A[[τ_{n}]]^{1}⟩

The term translation appears in Figure 16. In this translation, values are translated to both a value and a series of declarations that are used to construct that value. For non-tuple values, that series of declarations will be null (denoted by ϵ). The variables y_{i}, which are used internally by the translation, are always assumed fresh. When e is let d⃗ in E, we write let d⃗′ in e to mean let d⃗, d⃗′ in E.

Lemma 5.1 ⊢_{H} P if and only if there exists P′ such that ⊢_{H} P ⇝^{alloc} P′.

Lemma 5.2 (Allocation Type Correctness) If ⊢_{H} P ⇝^{alloc} P′ then ⊢_{A} P′.

The factorial example after application of the explicit allocation translation appears in Figure 17.

6 Typed Assembly Language

The final compilation stage, code generation, converts λ^{A} to TAL. All of the major typing constructs in TAL are present in λ^{A} and, indeed, code generation is largely syntactic. To summarize the type structure at this point, there is a combined abstraction mechanism that may simultaneously abstract a type environment, a set of type arguments, and a set of value arguments. Values of these types may be partially applied to type environments and remain values. There are existential types to support closures and other data abstractions. Finally, there are n-tuples with flags on the fields indicating whether the field has been initialized.

A key technical distinction between λ^{A} and TAL is that λ^{A} uses alpha-varying variables, whereas TAL uses register names, which like labels on records, do not alpha-vary.^{2} Following standard practice, we assume an infinite supply of registers. Mapping to a language with a finite number of registers may be performed by spilling registers into a tuple, and reloading values from this tuple when necessary.

One of the consequences of this aspect of TAL is that a register calling convention must be used in code generation, and that calling convention must be made explicit in the types. Hence TAL includes the type ∀[α⃗]{r1:τ_{1}, …, rn:τ_{n}}, which is used to describe entry points of code blocks (i.e., code labels) and is the TAL analog of the λ^{A} function type, ∀[α⃗].(τ_{1}, …, τ_{n}) → void. The key difference is that we assign fixed registers to the arguments of the code. Intuitively, to jump to a block of code of this type, the type variables α⃗ must be suitably instantiated, and registers r1 through rn must contain values of type τ_{1} through τ_{n}, respectively.

2Indeed, the register file may be viewed as a record, and register names as field labels for this record.

{FTV (τ) ⊆ Δ \atop Δ ⊢_{A} τ}

Ψ; Δ; Γ ⊢_{A} x : τ (Γ(x) = τ) Ψ; Δ; Γ ⊢_{A} ℓ : τ (Ψ(ℓ) = τ) Ψ; Δ; Γ ⊢_{A} i : int
Δ ⊢_{A} σ Ψ; Δ; Γ ⊢_{A} v : ∀[α, β⃗].(τ⃗) → void
Ψ; Δ; Γ ⊢_{A} v[σ] : ∀[β⃗].(τ⃗[σ/α]) → void
Δ ⊢_{A} τ Ψ; Δ; Γ ⊢_{A} v : τ′[τ/α]
Ψ; Δ; Γ ⊢_{A} pack [τ, v] as ∃α.τ′ : ∃α.τ′
Ψ; Δ; Γ ⊢_{A} v : ∀[ ].(τ_{1}, …, τ_{n}) → void Ψ; Δ; Γ ⊢_{A} v_{i} : τ_{i}
Ψ; Δ; Γ ⊢_{A} let in v(v_{1}, …, v_{n})
Ψ; Δ; Γ ⊢_{A} v : int Ψ; Δ; Γ ⊢_{A} e_{1} Ψ; Δ; Γ ⊢_{A} e_{2}
Ψ; Δ; Γ ⊢_{A} let in if0 (v, e_{1}, e_{2})

Ψ; Δ; Γ ⊢_{A} v : τ

Ψ; Δ; Γ ⊢_{A} let in halt[τ]v
Ψ; Δ; Γ ⊢_{A} v : τ Ψ; Δ; Γ{x:τ} ⊢_{A} let d⃗ in e
Ψ; Δ; Γ ⊢_{A} let x = v, d⃗ in e

(x ∉ Γ)
Ψ; Δ; Γ ⊢_{A} v : ⟨τ_{1}^{φ_{1}}, …, τ_{n}^{φ_{n}}⟩ Ψ; Δ; Γ{x:τ_{i}} ⊢_{A} let d⃗ in e
Ψ; Δ; Γ ⊢_{A} let x = π_{i}(v), d⃗ in e

(φ_{i} = 1, x ∉ Γ, 1 ≤ i ≤ n)
Ψ; Δ; Γ ⊢_{A} v_{1} : int Ψ; Δ; Γ ⊢_{A} v_{2} : int Ψ; Δ; Γ{x:int} ⊢_{A} let d⃗ in e
Ψ; Δ; Γ ⊢_{A} let x = v_{1} p v_{2}, d⃗ in e

(x ∉ Γ)
Ψ; Δ; Γ ⊢_{A} v : ∃α.τ Ψ; Δα; Γ{x:τ} ⊢_{A} let d⃗ in e
Ψ; Δ; Γ ⊢_{A} let [α, x] = unpack v, d⃗ in e

(x ∉ Γ, α ∉ Δ)
Δ ⊢_{A} τ_{i} Ψ; Δ; Γ{x:⟨τ_{1}^{0}, …, τ_{n}^{0}⟩} ⊢_{A} let d⃗ in e
Ψ; Δ; Γ ⊢_{A} let x = malloc[τ_{1}, …, τ_{n}], d⃗ in e

(x ∉ Γ)
Ψ; Δ; Γ ⊢_{A} v : ⟨τ_{1}^{φ_{1}}, …, τ_{n}^{φ_{n}}⟩ Ψ; Δ; Γ ⊢_{A} v′ : τ_{i}

Ψ; Δ; Γ{x:⟨τ_{1}^{φ_{1}}, …, τ_{i−1}^{φ_{i−1}}, τ_{i}^{1}, τ_{i+1}^{φ_{i+1}}, …, τ_{n}^{φ_{n}}⟩} ⊢_{A} let d⃗ in e Ψ; Δ; Γ ⊢_{A} let x = v[i] ← v′, d⃗ in e

(x ∉ Γ, 1 ≤ i ≤ n)
α⃗ ⊢_{A} τ_{i} Ψ; α⃗; {x_{1}:τ_{1}, …, x_{n}:τ_{n}} ⊢_{A} e

Ψ ⊢_{A} ℓ ↦ code[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e : ℓ ↦ ∀[α⃗].(τ_{1}, …, τ_{n}) → void

∅ ⊢_{A} τ_{i} Ψ ⊢_{A} b_{i} : ℓ_{i} ↦ τ_{i} Ψ; ∅; ∅ ⊢_{A} e

⊢_{A} letrec b_{1}, …, b_{n} in e ( \begin{matrix}Ψ = ℓ_{1}:τ_{1}, …, ℓ_{n}:τ_{n} \\ ℓ_{j} ≠ ℓ_{k} when j ≠ k \end{matrix} )

Figure 14: Static Semantics of λ^{A}

A[[α]] =^{def} α
A[[int]] =^{def} int
A[[∀[α⃗].(τ⃗) → void]] =^{def} ∀[α⃗].(A[[τ⃗]]) → void
A[[⟨τ_{1}, …, τ_{n}⟩]] =^{def} ⟨A[[τ_{1}]]^{1}, …, A[[τ_{n}]]^{1}⟩
A[[∃α.τ]] =^{def} ∃α.A[[τ]]

Figure 15: Type Translation from λ^{H} to λ^{A}

Another technical point is that registers may contain only word values, which are integers, pointers into the heap (i.e., labels), and instantiated or packed word values. Tuples and code blocks are large values and must be heap allocated. In this manner, TAL makes the layout of data in memory explicit.

In the remainder of this section, we present the syntax of TAL (Section 6.1), its dynamic semantics (Section 6.2), and its full static semantics (Section 6.3). Finally, we sketch the translation from λ^{A} to TAL (Section 6.4).

6.1 TAL Syntax

We present the full syntax of TAL in Figure 18. A TAL abstract machine or program consists of a heap, a register file and a sequence of instructions. The heap is a mapping of labels to heap values, which are tuples and code. The register file is a mapping of registers (ranged over by the metavariable r) to word values. Heaps, register files, and their respective types are not considered syntactically correct if they repeat labels or registers. When r appears in R, the notation R{r ↦ w} represents the register file R with the r binding replaced with w, and a similar notation is used for register file types; if r does not appear in R, the indicated binding is merely added, as usual.

Although heap values are not word values, the labels that point to them are. The other word values are integers, instantiations of word values, existential packages, and junk values (?τ), which are used by the operational semantics to represent uninitialized data. A small value is either a word value, a register, or an instantiated or packed small value. The distinction between word and small values is drawn because a register must contain a word, not another register. Code blocks are linear sequences of instructions that abstract a set of type variables, and state their register assumptions. The sequence of instructions is always terminated by a jmp or halt instruction. Expressions that differ only by alpha-variation (of type variables) are considered identical, as are programs that differ only in the order of fields in a heap or register file.

6.2 TAL Operational Semantics

The operational semantics of TAL is presented in Figure 19 as a deterministic rewriting system P ⟼ P′ that maps programs to programs. Although, as discussed above, we ultimately intend a type-erasure interpretation, we do not erase the types from the operational semantics presented here, so that we may more easily state and prove a subject reduction theorem (Lemma 6.1). The

Ψ; Δ; Γ ⊢_{H} x : τ ⇝^{alloc} x, ϵ (Γ(x) = τ)  Ψ; Δ; Γ ⊢_{H} ℓ : τ ⇝^{alloc} ℓ, ϵ (Ψ(ℓ) = τ)

Ψ; Δ; Γ ⊢_{H} i : int ⇝^{alloc} i, ϵ

Ψ; Δ; Γ ⊢_{H} v_{i} : τ_{i} ⇝^{alloc} v′_{i}, d⃗_{i}

Ψ; Δ; Γ ⊢_{H} ⟨v_{1}, …, v_{n}⟩ : ⟨τ_{1}, …, τ_{n}⟩ ⇝^{alloc} y_{n}, (d⃗_{1}, …, d⃗_{n}, ; y_{0} = malloc[A[[τ_{1}]], …, A[[τ_{n}]]], ; y_{1} = y_{0}[1] ← v′_{1}, ; ⋮ ; y_{n} = y_{n−1}[n] ← v′_{n})

Δ ⊢_{H} σ Ψ; Δ; Γ ⊢_{H} v : ∀[α, β⃗](τ⃗) → void ⇝^{alloc} v′, d⃗
Ψ; Δ; Γ ⊢_{H} v[σ] : ∀[β⃗](τ⃗[σ/α]) → void ⇝ v′[A[[σ]]], d⃗
Δ ⊢_{H} τ Ψ; Δ; Γ ⊢_{H} v : τ′[τ/α] ⇝^{alloc} v′, d⃗

Ψ; Δ; Γ ⊢_{H} pack [τ, v] as ∃α.τ′ : ∃α.τ′ ⇝^{alloc} pack [A[[τ]], v′] as A[[∃α.τ′]], d⃗

Ψ; Δ; Γ ⊢_{H} v : ∀[ ].(τ_{1}, …, τ_{n}) → void ⇝^{alloc} v′, d⃗ Ψ; Δ; Γ ⊢_{H} v_{i} : τ_{i} ⇝^{alloc} v′_{i}, d⃗_{i}

Ψ; Δ; Γ ⊢_{H} v(v_{1}, …, v_{n}) ⇝^{alloc} let d⃗, d⃗_{1}, …, d⃗_{n} in v′(v′_{1}, …, v′_{n})

Ψ; Δ; Γ ⊢_{H} v : int ⇝^{alloc} v′, d⃗ Ψ; Δ; Γ ⊢_{H} e_{1} ⇝^{alloc} e′_{1} Ψ; Δ; Γ ⊢_{H} e_{2} ⇝^{alloc} e′_{2}
Ψ; Δ; Γ ⊢_{H} if0 (v, e_{1}, e_{2}) ⇝^{alloc} let d⃗ in if0 (v′, e′_{1}, e′_{2})
Ψ; Δ; Γ ⊢_{H} v : τ ⇝^{alloc} v′, d⃗
Ψ; Δ; Γ ⊢_{H} halt[τ]v ⇝ let d⃗ in halt[A[[τ]]]v′
Ψ; Δ; Γ ⊢_{H} v : τ ⇝^{alloc} v′, d⃗ Ψ; Δ; Γ{x:τ} ⊢_{H} e ⇝^{alloc} e′

Ψ; Δ; Γ ⊢_{H} let x = v in e ⇝^{alloc} let d⃗, x = v′ in e′

(x ∉ Γ)
Ψ; Δ; Γ ⊢_{H} v : ⟨τ_{1}, …, τ_{n}⟩ ⇝^{alloc} v′, d⃗ Ψ; Δ; Γ{x:τ_{i}} ⊢_{H} e ⇝^{alloc} e′

Ψ; Δ; Γ ⊢_{H} let x = π_{i}(v) in e ⇝^{alloc} let d⃗, x = π_{i}(v′) in e′

(x ∉ Γ, 1 ≤ i ≤ n)
Ψ; Δ; Γ ⊢_{H} v_{1} : int ⇝^{alloc} v′_{1}, d⃗_{1} Ψ; Δ; Γ ⊢_{H} v_{2} : int ⇝^{alloc} v′_{2}, d⃗_{2} Ψ; Δ; Γ{x:int} ⊢_{H} e ⇝^{alloc} e′

Ψ; Δ; Γ ⊢_{H} let x = v_{1} p v_{2} in e ⇝^{alloc} let d⃗_{1}, d⃗_{2}, x = v′_{1} p v′_{2} in e′

(x ∉ Γ)
Ψ; Δ; Γ ⊢_{H} v : ∃α.τ ⇝^{alloc} v′, d⃗ Ψ; Δα; Γ{x:τ} ⊢_{H} e ⇝^{alloc} e′

Ψ; let [α, x] = unpack v in e ⇝^{alloc} let d⃗, [α, x] = unpack v′ in e′

(x ∉ Γ, α ∉ Δ)

α⃗ ⊢_{H} τ_{i} Ψ; α⃗; {x_{1}:τ_{1}, …, x_{n}:τ_{n}} ⊢_{H} e ⇝^{alloc} e′

Ψ ⊢_{H} ℓ ↦ code[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e : ℓ ↦ ∀[α⃗].(τ_{1}, …, τ_{n}) → void ⇝^{alloc}

ℓ ↦ code[α⃗](x_{1}:A[[τ_{1}]], …, x_{n}:A[[τ_{n}]]).e′

∅ ⊢_{H} τ_{i} Ψ ⊢_{H} b_{i} : ℓ_{i} ↦ τ_{i} ⇝^{alloc} b′_{i} Ψ; ∅; ∅ ⊢_{H} e ⇝^{alloc} e′

⊢_{H} letrec b_{1}, …, b_{n} in e ⇝^{alloc} letrec b′_{1}, …, b′_{n} in e′ ( \begin{matrix}Ψ = ℓ_{1}:τ_{1}, …, ℓ_{n}:τ_{n} \\ ℓ_{j} ≠ ℓ_{k} when j ≠ k \end{matrix} )

Figure 16: Term Translation from λ^{H} to λ^{A} letrec ℓ_{fact} ↦ code[ ](env:⟨⟩, n:int, k:τ_{k}).

let in if0 (n,

let [β, k_{unpack}] = unpack k k_{code} = π_{0}(k_{unpack}) k_{env} = π_{1}(k_{unpack})

in k_{code}(k_{env}, 1), let x = n − 1

y_{5} = malloc[int, τ_{k}] y_{6} = y_{5}[1] ← n y_{7} = y_{6}[2] ← k y_{8} = malloc[(⟨int^{1}, τ_{k}^{1}⟩, int) → void, ⟨int^{1}, τ_{k}^{1}⟩,] y_{9} = y_{8}[1] ← ℓ_{cont} y_{10} = y_{9}[2] ← y_{7}

in ℓ_{fact}(env, x, pack [⟨int^{1}, τ_{k}^{1}⟩, y_{10}] as τ_{k}))

ℓ_{cont} ↦ code[ ](env:⟨int^{1}, τ_{k}^{1}⟩, y:int).

let n = π_{0}(env) k = π_{1}(env) z = n × y [β, k_{unpack}] = unpack k k_{code} = π_{0}(k_{unpack}) k_{env} = π_{1}(k_{unpack})

in k_{code}(k_{env}, z)

ℓ_{halt} ↦ code[ ](env:⟨⟩, n:int). let in halt[int](n) in

let y_{0} = malloc[ ] y_{1} = malloc[ ] y_{2} = malloc[(⟨⟩, int) → void, ⟨⟩] y_{3} = y_{2}[1] ← ℓ_{halt} y_{4} = y_{3}[2] ← y_{1}

in ℓ_{fact}(y_{0}, 6, pack [⟨⟩, y_{4}] as τ_{k}) where τ_{k} is ∃α.⟨(α, int) → void^{1}, α^{1}⟩

Figure 17: Factorial in λ^{A}

types  τ ::= α | int | ∀[α⃗].Γ | ⟨τ_{1}^{φ_{1}}, …, τ_{n}^{φ_{n}}⟩ | ∃α.τ
initialization flags  φ ::= 0 | 1
heap types  Ψ ::= {ℓ_{1}:τ_{1}, …, ℓ_{n}:τ_{n}}
register file types  Γ ::= {r_{1}:τ_{1}, …, r_{n}:τ_{n}}
type contexts  Δ ::= α⃗
registers  r ::= r1 | r2 | r3 | ⋯
word values  w ::= ℓ | i | ?τ | w[τ] | pack [τ, w] as τ′
small values  v ::= r | w | v[τ] | pack [τ, v] as τ′
heap values  h ::= ⟨w_{1}, …, w_{n}⟩ | code[α⃗]Γ.S
heaps  H ::= {ℓ_{1} ↦ h_{1}, …, ℓ_{n} ↦ h_{n}}
register files  R ::= {r_{1} ↦ w_{1}, …, r_{n} ↦ w_{n}}
instructions  ι ::= add r_{d}, r_{s}, v | bnz r, v | ld r_{d}, r_{s}[i] | malloc r_{d}[τ⃗] | mov r_{d}, v |

mul r_{d}, r_{s}, v | st r_{d}[i], r_{s} | sub r_{d}, r_{s}, v | unpack[α, r_{d}], v

instruction sequences  S ::= ι; S | jmp v | halt[τ]
programs  P ::= (H, R, S)

Figure 18: Syntax of TAL

well-formed terminal configurations of the rewriting system have the form (H, R{r1 ↦ w}, halt[τ]). This corresponds to a machine state where the register r1 contains the value computed by the computation. All other terminal configurations are considered to be “stuck” programs.

If we erase the types from the instructions, then their meaning is intuitively clear and there is a one-to-one correspondence with conventional assembly language instructions. The two exceptions to this are the unpack and malloc instructions, which are discussed below.

Intuitively, the ld r_{d}, r_{s}[i] instruction loads the i^{th} component (counting from 0) of the tuple bound to the label in r_{s}, and places this word value in r_{d}. Conversely, st r_{d}[i], r_{s} places the word value in r_{s} at the i^{th} position of the tuple bound to the label in r_{d}. The instruction jmp v, where v is a value of the form ℓ[τ⃗], transfers control to the code bound to the label ℓ, instantiating the abstracted type variables of ℓ with τ⃗. The bnz r, v instruction tests the value in r to see if it is zero. If so, then control continues with the next instruction. Otherwise control is transferred to v as with the jmp instruction.

The instruction unpack[α, r_{d}], v, where v is a value of the form pack [τ′, v′] as τ, is evaluated by substituting τ′ for α in the remainder of the sequence of instructions currently being executed, and by binding the register r_{d} to the value v′. If types are erased, the unpack instruction can be implemented with a mov instruction.

As at the λ^{A} level, malloc r_{d}[τ_{1}, …, τ_{n}] allocates a fresh, uninitialized tuple in the heap and binds the address of this tuple to r_{d}. Of course, real machines do not provide a primitive malloc instruction. Our intention is that, as types are erased, malloc is expanded into a fixed instruction sequence that allocates a tuple of the appropriate size. Because this instruction sequence is abstract, it prevents optimization from re-ordering and interleaving these underlying instructions with the surrounding TAL code. However, this is the only instruction sequence that is abstract in TAL.

(H, R, S) ⟼ P where

if S =  then P =
add r_{d}, r_{s}, v; S′  (H, R{r_{d} ↦ R(r_{s}) + R̂(v)}, S′)

and similarly for mul and sub

bnz r, v; S′  (H, R, S′)

when R(r) = 0

bnz r, v; S′  (H, R, S′′[τ⃗/α⃗])
when R(r) = i and i ≠ 0 where R̂(v) = ℓ[τ⃗]

and H(ℓ) = code[α⃗]Γ.S′′

jmp v  (H, R, S′[τ⃗/α⃗])

where R̂(v) = ℓ[τ⃗]

and H(ℓ) = code[α⃗]Γ.S′

ld r_{d}, r_{s}[i]; S′  (H, R{r_{d} ↦ w_{i}}, S′)

where R(r_{s}) = ℓ

and H(ℓ) = ⟨w_{0}, …, w_{n−1}⟩ with 0 ≤ i < n

malloc r_{d}[τ_{1}, …, τ_{n}]; S′ (H{ℓ ↦ ⟨?τ_{1}, …,?τ_{n}⟩}, R{r_{d} ↦ ℓ}, S′)

where ℓ ∉ H

mov r_{d}, v; S′  (H, R{r_{d} ↦ R̂(v)}, S′)
st r_{d}[i], r_{s}; S′  (H{ℓ ↦ ⟨w_{0}, …, w_{i−1}, R(r_{s}), w_{i+1}, …, w_{n−1}⟩}, R, S′)

where R(r_{d}) = ℓ

and H(ℓ) = ⟨w_{0}, …, w_{n−1}⟩ with 0 ≤ i < n

unpack[α, r_{d}], v; S′  (H, R{r_{d} ↦ w}, S′[τ/α])

where R̂(v) = pack [τ, w] as τ′

Where R̂(v) = \{ \begin{matrix}R(r) & when v = r \\ w & when v = w \\ R̂(v′)[τ] & when v = v′[τ] \\ pack [τ, R̂(v′)] as τ′ & when v = pack [τ, v′] as τ′ \end{matrix}

Figure 19: Operational Semantics of TAL

Real machines also have a finite amount of heap space. It is straightforward to link our TAL to a conservative garbage collector [9] in order to reclaim unused heap values. Support for an accurate collector would require introducing tags so that we may distinguish pointers from integers, or else require a type-passing interpretation [43, 30]. The tagging approach is readily accomplished in our framework.

6.3 TAL Static Semantics

The static semantics for TAL appears in Figures 21 and 22 and consists of thirteen judgments, summarized in Figure 20 and elaborated briefly below. The static semantics is inspired by and follows the conventions of Morrisett and Harper’s λ_{gc}^{→∀} [30].

Judgment  Meaning
Δ ⊢_{TAL} τ type  τ is a well-formed type
⊢_{TAL} Ψ htype  Ψ is a well-formed heap type
Δ ⊢_{TAL} Γ rftype  Γ is a well-formed register file type
Δ ⊢_{TAL} τ_{1} ≤ τ_{2} type  τ_{1} is a subtype of τ_{2}
Δ ⊢_{TAL} Γ_{1} ≤ Γ_{2} rftype Γ_{1} is register file subtype of Γ_{2}
⊢_{TAL} H : Ψ heap  H is a well-formed heap of heap type Ψ
Ψ ⊢_{TAL} R : Γ regfile  R is a well-formed register file of register file type Γ
Ψ ⊢_{TAL} h : τ hval  h is a well-formed heap value of type τ
Ψ; Δ ⊢_{TAL} w : τ wval w is a well-formed word value of type τ
Ψ; Δ ⊢_{TAL} w : τ^{φ} fwval w is a well-formed word value of flagged type τ^{φ}

(i.e., w has type τ or w is ?τ and φ is 0)

Ψ; Δ; Γ ⊢_{TAL} v : τ  v is a well-formed small value of type τ
Ψ; Δ; Γ ⊢_{TAL} S  S is a well-formed instruction sequence
⊢_{TAL} P  P is a well-formed program

Figure 20: TAL Static Semantic Judgments

The first five judgments state well-formedness and subtyping of various sorts of types. Each of these judgments are relative to a type context except the heap type well-formedness judgment; heaps and heap types are required to be closed, so no type context is used. Next are two judgments for assigning types to heaps and to register files; neither heaps nor register files may contain free type variables, but register files may contain references to the heap.

The next four judgments are for assigning types to values. In addition to one rule for each sort of value, there is a rule for assigning flagged types to word values: the junk value ?τ may not be assigned any regular type, but it may be assigned the flagged type τ^{0}. Each value sort may contain references to the heap, all but heap values may contain free type variables, but (as discussed above) only small values may contain registers. The final two judgments assert well-formedness of instruction sequences and programs.

A few additional words are merited on the two subtyping judgments. Neither of these are intended to support subtyping in the usual sense, although they could be expanded to do so. Instead, they are used to allow the forgetting of information in particular places where necessary. The subtyping judgment makes it possible to forget that a field of a tuple has been initialized. This is used in the subject reduction argument (Lemma 6.1) where it is sometimes necessary that references to an initialized tuple be given the old uninitialized type. The register file subtyping judgment makes it possible to forget the types of some registers. This makes it possible to jump to a code block when “too many” registers are defined.

The following two lemmas and their corollary establish type safety for TAL. Their proofs appear in Appendix A.

Lemma 6.1 (Subject Reduction) If ⊢_{TAL} P and P ⟼ P′, then ⊢_{TAL} P′.

Δ ⊢_{TAL} τ type ⊢_{TAL} Ψ htype Δ ⊢_{TAL} Γ rftype (type)

FTV (τ) ⊆ Δ
Δ ⊢_{TAL} τ type

(heap-type)

∅ ⊢_{TAL} τ_{i} type
⊢_{TAL} {ℓ_{1}:τ_{1}, …, ℓ_{n}:τ_{n}} htype

(reg-type)

Δ ⊢_{TAL} τ_{i} type

Δ ⊢_{TAL} {r_{1}:τ_{1}, …, r_{n}:τ_{n}} rftype

Δ ⊢_{TAL} τ_{1} ≤ τ_{2} type Δ ⊢_{TAL} Γ_{1} ≤ Γ_{2} rftype (reflex)

Δ ⊢_{TAL} τ type
Δ ⊢_{TAL} τ ≤ τ type

(trans)

Δ ⊢_{TAL} τ_{1} ≤ τ_{2} type Δ ⊢_{TAL} τ_{2} ≤ τ_{3} type
Δ ⊢_{TAL} τ_{1} ≤ τ_{3} type

(0-1)

Δ ⊢_{TAL} τ_{i} type

Δ ⊢_{TAL} ⟨τ_{1}^{φ_{1}}, …, τ_{i−1}^{φ_{i−1}}, τ_{i}^{1}, τ_{i+1}^{φ_{i+1}}, …, τ_{n}^{φ_{n}}⟩ ≤ ⟨τ_{1}^{φ_{1}}, …, τ_{i−1}^{φ_{i−1}}, τ_{i}^{0}, τ_{i+1}^{φ_{i+1}}, …, τ_{n}^{φ_{n}}⟩ type

(weaken) Δ ⊢_{TAL} τ_{i} type (for 1 ≤ i ≤ m) Δ ⊢_{TAL} {r_{1} : τ_{1}, …, r_{m} : τ_{m}} ≤ {r_{1} : τ_{1}, …, r_{n} : τ_{n}} rftype (m ≥ n)

⊢_{TAL} P ⊢_{TAL} H : Ψ heap Ψ ⊢_{TAL} R : Γ regfile (prog)

⊢_{TAL} H : Ψ heap Ψ ⊢_{TAL} R : Γ regfile Ψ; ∅; Γ ⊢_{TAL} S
⊢_{TAL} (H, R, S)
(heap) ⊢_{TAL} Ψ htype Ψ ⊢_{TAL} h_{i} : τ_{i} hval ⊢_{TAL} {ℓ_{1} ↦ h_{1}, …, ℓ_{n} ↦ h_{n}} : Ψ heap (Ψ = {ℓ_{1}:τ_{1}, …, ℓ_{n}:τ_{n}})
(reg) Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i} wval (for 1 ≤ i ≤ m) Ψ ⊢_{TAL} {r_{1} ↦ w_{1}, …, r_{m} ↦ w_{m}} : {r_{1} ↦ τ_{1}, …, r_{n} ↦ τ_{n}} regfile (m ≥ n)

Ψ ⊢_{TAL} h : τ hval Ψ; Δ ⊢_{TAL} w : τ wval Ψ; Δ ⊢_{TAL} w : τ^{φ} fwval Ψ; Δ; Γ ⊢_{TAL} v : τ (tuple)

Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i}^{φ_{i}} fwval
Ψ ⊢_{TAL} ⟨w_{1}, …, w_{n}⟩ : ⟨τ_{1}^{φ_{1}}, …, τ_{n}^{φ_{n}}⟩ hval

(code)

α⃗ ⊢_{TAL} Γ rftype Ψ; α⃗; Γ ⊢_{TAL} S
Ψ ⊢_{TAL} code[α⃗]Γ.S : ∀[α⃗].Γ hval
(label) Δ ⊢_{TAL} τ′ ≤ τ type Ψ; Δ ⊢_{TAL} ℓ : τ wval (Ψ(ℓ) = τ′)  (int) Ψ; Δ ⊢_{TAL} i : int wval

(tapp-word)

Δ ⊢_{TAL} τ type Ψ; Δ ⊢_{TAL} w : ∀[α, β⃗].Γ wval
Ψ; Δ ⊢_{TAL} w[τ] : ∀[β⃗].Γ[τ/α] wval

(pack-word)

Δ ⊢_{TAL} τ type Ψ; Δ ⊢_{TAL} w : τ′[τ/α] wval
Ψ; Δ ⊢_{TAL} pack [τ, w] as ∃α.τ′ : ∃α.τ′ wval

(init)

Ψ; Δ ⊢_{TAL} w : τ wval
Ψ; Δ ⊢_{TAL} w : τ^{φ} fwval

(uninit)

Δ ⊢_{TAL} τ type
Ψ; Δ ⊢_{TAL} ?τ : τ^{0} fwval

(reg-val)

Ψ; Δ; Γ ⊢_{TAL} r : τ (Γ(r) = τ)

(word-val)

Ψ; Δ ⊢_{TAL} w : τ wval
Ψ; Δ; Γ ⊢_{TAL} w : τ

(tapp-val)

Δ ⊢_{TAL} τ type Ψ; Δ; Γ ⊢_{TAL} v : ∀[α, β⃗].Γ′
Ψ; Δ; Γ ⊢_{TAL} v[τ] : ∀[β⃗].Γ′[τ/α]

(pack-val)

Δ ⊢_{TAL} τ type Ψ; Δ; Γ ⊢_{TAL} v : τ′[τ/α]
Ψ; Δ; Γ ⊢_{TAL} pack [τ, v] as ∃α.τ′ : ∃α.τ′

Figure 21: Static Semantics of TAL (except instructions)

Ψ; Δ; Γ ⊢_{TAL} S

(s-arith) Ψ; Δ; Γ ⊢_{TAL} r_{s} : int  Ψ; Δ; Γ ⊢_{TAL} v : int Ψ; Δ; Γ{r_{d}:int} ⊢_{TAL} S Ψ; Δ; Γ ⊢_{TAL} arith r_{d}, r_{s}, v; S (arith ∈ {add, mul, sub})

(s-bnz)

Ψ; Δ; Γ ⊢_{TAL} r : int Ψ; Δ; Γ ⊢_{TAL} v : ∀[ ].Γ′

Δ ⊢_{TAL} Γ ≤ Γ′ rftype Ψ; Δ; Γ ⊢_{TAL} S
Ψ; Δ; Γ ⊢_{TAL} bnz r, v; S
(s-ld) Ψ; Δ; Γ ⊢_{TAL} r_{s} : ⟨τ_{0}^{φ_{0}}, …, τ_{n−1}^{φ_{n−1}}⟩ Ψ; Δ; Γ{r_{d}:τ_{i}} ⊢_{TAL} S Ψ; Δ; Γ ⊢_{TAL} ld r_{d}, r_{s}[i]; S (φ_{i} = 1, 0 ≤ i < n)

(s-malloc)

Δ ⊢_{TAL} τ_{i} type Ψ; Δ; Γ{r_{d}:⟨τ_{1}^{0}, …, τ_{n}^{0}⟩} ⊢_{TAL} S
Ψ; Δ; Γ ⊢_{TAL} malloc r_{d}[τ_{1}, …, τ_{n}]; S

(s-mov)

Ψ; Δ; Γ ⊢_{TAL} v : τ Ψ; Δ; Γ{r_{d} : τ} ⊢_{TAL} S
Ψ; Δ; Γ ⊢_{TAL} mov r_{d}, v; S
(s-sto) Ψ; Δ; Γ ⊢_{TAL} r_{d} : ⟨τ_{0}^{φ_{0}}, …, τ_{n−1}^{φ_{n−1}}⟩  Ψ; Δ; Γ ⊢_{TAL} r_{s} : τ_{i} Ψ; Δ; Γ{r_{d}:⟨τ_{0}^{φ_{0}}, …, τ_{i−1}^{φ_{i−1}}, τ_{i}^{1}, τ_{i+1}^{φ_{i+1}}, …, τ_{n−1}^{φ_{n−1}}⟩} ⊢_{TAL} S Ψ; Δ; Γ ⊢_{TAL} st r_{d}[i], r_{s}; S (0 ≤ i < n)
(s-unpack) Ψ; Δ; Γ ⊢_{TAL} v : ∃α.τ Ψ; Δα; Γ{r_{d}:τ} ⊢_{TAL} S Ψ; Δ; Γ ⊢_{TAL} unpack[α, r_{d}], v; S (α ∉ Δ)

(s-jmp)

Ψ; Δ; Γ ⊢_{TAL} v : ∀[ ].Γ′ Δ ⊢_{TAL} Γ ≤ Γ′ rftype
Ψ; Δ; Γ ⊢_{TAL} jmp v

(s-halt)

Ψ; Δ; Γ ⊢_{TAL} r1 : τ
Ψ; Δ; Γ ⊢_{TAL} halt[τ]

Figure 22: Static Semantics of TAL instructions

T [[α]] =^{def} α
T [[int]] =^{def} int
T [[∀[α⃗].(τ_{1}, …, τ_{n}) → void]] =^{def} ∀[α⃗].{r1:T [[τ_{1}]], …, rn:T [[τ_{n}]]}
T [[⟨τ_{1}^{φ_{1}}, …, τ_{n}^{φ_{n}⟩}]] =^{def} ⟨T [[τ_{1}]]^{φ_{1}}, …, T [[τ_{n}]]^{φ_{n}}⟩
T [[∃α.τ]] =^{def} ∃α.T [[τ]]
T [[x_{1}:τ_{1}, …, x_{n}:τ_{n}]] =^{def} {r1:T [[τ_{1}]], …, rn:T [[τ_{n}]]}

Figure 23: Type Translation from λ^{A} to TAL

Lemma 6.2 (Progress) If ⊢_{TAL} P, then either there exists P′ such that P ⟼ P′ or P is of the form (H, R{r1 ↦ w}, halt[τ]).

Corollary 6.3 (Type Safety) If ⊢_{TAL} P, then there is no stuck P′ such that P ⟼^{∗} P′.

6.4 Code Generation

The type translation, T [[ ·]] from λ^{A} to TAL is straightforward. The only point of interest is the translation of function types, which must assign registers to value arguments:

T [[∀[α⃗](τ_{1}, ⋯, τ_{n}) → void]] =^{def} ∀[α⃗]{r1:T [[τ_{1}]], …, rn:T [[τ_{n}]]}

The term translation appears in Figures 24 and 25. In this translation, values are translated to small values, terms are translated to pairs of instruction sequences and heaps, blocks are translated to heaps, and programs are translated to programs. The translation for terms needs to heap allocate the false branch of if0 expressions, which requires the use of a fresh label. In the other translations of the compiler, variables used internally by the translation have always been assumed fresh, but, since labels have global scope, choosing fresh labels is not necessarily simple. Consequently, the translation handles fresh label generation explicitly by supplying a set of used labels to the term and block translation judgments. The translation uses the notation |Γ|, representing the number of bindings in Γ, and the notations \overline{H} and \overline{Ψ}, representing the sets of labels bound in H and Ψ.

Informally, terms are translated to instruction sequences as follows:

• x = v is mapped to mov r_{x}, v.

• x = π_{i}(v) is mapped to the sequence mov r_{x}, v; ld r_{x}, r_{x}[i − 1]

• x = v_{1} p v_{2} is mapped to the sequence mov r_{x}, v_{1} ; arith r_{x}, r_{x}, v_{2} where arith is the appropriate arithmetic instruction.

• [α, x] = unpack v is mapped to unpack[α, r_{x}], v.

• x = malloc[τ⃗] is mapped to malloc r_{x}[τ⃗].

Ψ; Δ; {x_{1}:τ_{1}, …, x_{n}:τ_{n}} ⊢_{A} x_{i} : τ_{i} ⇝^{TAL} ri (1 ≤ i ≤ n)
Ψ; Δ; Γ ⊢_{A} ℓ : τ ⇝^{TAL} ℓ (Ψ(ℓ) = τ)  Ψ; Δ; Γ ⊢_{A} i : int ⇝^{TAL} i
Δ ⊢_{A} σ Ψ; Δ; Γ ⊢_{A} v : ∀[α, β⃗].(τ⃗) → void ⇝^{TAL} v′
Ψ; Δ; Γ ⊢_{A} v[σ] : ∀[β⃗].(τ⃗[σ/α]) → void ⇝^{TAL} v′[T [[σ]]]
Δ ⊢_{A} τ Ψ; Δ; Γ ⊢_{A} v : τ′[τ/α] ⇝^{TAL} v′
Ψ; Δ; Γ ⊢_{A} pack [τ, v] as ∃α.τ′ : ∃α.τ′ ⇝^{TAL} pack [T [[τ]], v′] as T [[∃α.τ′]]
α⃗ ⊢_{A} τ_{i} Ψ; α⃗; {x_{1}:τ_{1}, …, x_{n}:τ_{n}} ⊢_{A} e | L ⇝^{TAL} S, H

Ψ ⊢_{A} ℓ ↦ code[α⃗](x_{1}:τ_{1}, …, x_{n}:τ_{n}).e : ℓ ↦ ∀[α⃗].(τ_{1}, …, τ_{n}) → void | L ⇝^{TAL}

H, ℓ ↦ code[α⃗]{r1:T [[τ_{1}]], …, rn:T [[τ_{n}]]}.S

Ψ ⊢_{A} b_{i} : ℓ_{i} ↦ τ_{i} | L_{i−1} ⇝^{TAL} H_{i} ∅ ⊢_{A} τ_{i}

Ψ; ∅; ∅ ⊢_{A} e | L_{n} ⇝^{TAL} S, H

⊢_{A} letrec b_{1}, …, b_{n} in e ⇝^{TAL} ((H_{1}, …, H_{n}, H), ∅, S) ( \begin{matrix}L_{i} = \overline{Ψ} ∪ \overline{H_{1}} ∪ ⋯ ∪ \overline{H_{i}} \\ Ψ = ℓ_{1}:τ_{1}, …, ℓ_{n}:τ_{n} \\ ℓ_{j} ≠ ℓ_{k} when j ≠ k \end{matrix} )

Figure 24: Program Translation from λ^{A} to TAL (except terms)

• x = v[i] ← v′ is mapped to the sequence:

mov r_{x}, v; mov r_{temp}, v′; st r_{x}[i − 1], r_{temp}

• v(v_{1}, …, v_{n}) is mapped to the sequence:

mov r_{temp_{1}}, v_{1} ; …; mov r_{temp_{n}}, v_{n}; movr1, r_{temp_{1}} ; …; movrn, r_{temp_{n}} ; jmp v

Note that the arguments cannot be moved immediately into the registers r1, …, rn because those registers may be used in later arguments.

• if0 (v, e_{1}, e_{2}) is mapped to the sequence:

mov r_{temp}, v; bnz r_{temp}, ℓ[α⃗] ; S_{1}

where ℓ is bound in the heap to code[α⃗]Γ.S_{2}, the translation of e_{i} is S_{i}, the free type variables of e_{2} are contained in α⃗, and Γ is the register file type corresponding to the free variables of e_{2}.

• halt[τ]v is mapped to the sequence movr1, v; halt[τ]

Lemma 6.4 ⊢_{A} P if and only if there exists P′ such that ⊢_{A} P ⇝^{TAL} P′

Lemma 6.5 (TAL Conversion Type Correctness) If b ⊢_{A} P ⇝^{TAL} P′ then ⊢_{TAL} P′.

Ψ; Δ; Γ ⊢_{A} v : ∀[ ].(τ_{1}, …, τ_{n}) → void ⇝^{TAL} v′ Ψ; Δ; Γ ⊢_{A} v_{i} : τ_{i} ⇝^{TAL} v′_{i}
Ψ; Δ; Γ ⊢_{A} let in v(v_{1}, …, v_{n}) | L ⇝^{TAL}
(movr(k + 1), v′_{1} ; …; movr(k + n), v′_{n};

movr1, r(k + 1) ; …; movrn, r(k + n) ; jmp v′), ϵ

(|Γ| = k)
Ψ; Δ; Γ ⊢_{A} v : int ⇝^{TAL} v′

Ψ; Δ; Γ ⊢_{A} e_{1} | L ⇝^{TAL} S_{1}, H_{1} Ψ; Δ; Γ ⊢_{A} e_{2} | L ∪ \overline{H_{1}} ⇝^{TAL} S_{2}, H_{2}

Ψ; Δ; Γ ⊢_{A} let in if0 (v, e_{1}, e_{2}) | L ⇝^{TAL}

(mov r, v; bnz r, ℓ[α⃗] ; S_{1}), (H_{1}, H_{2}, ℓ ↦ code[α⃗]T [[Γ]].S_{2}) ( \begin{matrix}ℓ ∉ L ∪ \overline{H_{1}} ∪ \overline{H_{2}} \\ r = r(|Γ| + 1) \\ Δ = α⃗ \end{matrix} )

Ψ; Δ; Γ ⊢_{A} v : τ ⇝^{TAL} v′

Ψ; Δ; Γ ⊢_{A} let in halt[τ]v | L ⇝^{TAL} (movr1, v′; halt[T [[τ]]]), ϵ

Ψ; Δ; Γ ⊢_{A} v : τ ⇝^{TAL} v′ Ψ; Δ; Γ{x:τ} ⊢_{A} let d⃗ in e | L ⇝^{TAL} S, H

Ψ; Δ; Γ ⊢_{A} let x = v, d⃗ in e | L ⇝^{TAL}⇝ (mov r, v′; S), H ( \begin{matrix}r = r(|Γ| + 1) \\ x ∉ Γ \end{matrix} )

Ψ; Δ; Γ ⊢_{A} v : ⟨τ_{1}^{φ_{1}}, …, τ_{n}^{φ_{n}}⟩ ⇝^{TAL} v′ Ψ; Δ; Γ{x:τ_{i}} ⊢_{A} let d⃗ in e | L ⇝^{TAL} S, H

Ψ; Δ; Γ ⊢_{A} let x = π_{i}(v), d⃗ in e | L ⇝^{TAL} (mov r, v′; ld r, r[i − 1] ; S), H ( \begin{matrix}r = r(|Γ| + 1) \\ φ_{i} = 1 \\ x ∉ Γ \\ 1 ≤ i ≤ n \end{matrix} )

Ψ; Δ; Γ ⊢_{A} v_{1} : int ⇝^{TAL} v′_{1} Ψ; Δ; Γ ⊢_{A} v_{2} : int ⇝^{TAL} v′_{2}

Ψ; Δ; Γ{x:int} ⊢_{A} let d⃗ in e | L ⇝^{TAL} S, H

Ψ; Δ; Γ ⊢_{A} let x = v_{1} p v_{2}, d⃗ in e | L ⇝^{TAL} (mov r, v′_{1} ; arith_{p} r, r, v′_{2} ; S), H

                                                      ( \begin{matrix}r = r(|Γ| + 1) \\ arith_{+} = add \\ arith_{−} = sub \\ arith_{×} = mul \\ x ∉ Γ \end{matrix} )

Ψ; Δ; Γ ⊢_{A} v : ∃α.τ ⇝^{TAL} v′ Ψ; Δα; Γ{x:τ} ⊢_{A} let d⃗ in e | L ⇝^{TAL} S, H

Ψ; Δ; Γ ⊢_{A} let [α, x] = unpack v, d⃗ in e | L ⇝^{TAL} (unpack[α, r], v′; S), H

( \begin{matrix}r = r(|Γ| + 1) \\ x ∉ Γ \\ α ∉ Δ \end{matrix} )
Δ ⊢_{A} τ_{i} Ψ; Δ; Γ{x:⟨τ_{1}^{0}, …, τ_{n}^{0}⟩} ⊢_{A} let d⃗ in e | L ⇝^{TAL} S, H

Ψ; Δ; Γ ⊢_{A} let x = malloc[τ_{1}, …, τ_{n}], d⃗ in e | L ⇝^{TAL}

(malloc[T [[τ_{1}]], …, T [[τ_{n}]]] ; S), H ( \begin{matrix}r = r(|Γ| + 1) \\ x ∉ Γ \end{matrix} )

Ψ; Δ; Γ ⊢_{A} v_{1} : ⟨τ_{1}^{φ_{1}}, …, τ_{n}^{φ_{n}}⟩ ⇝^{TAL} v′_{1} Ψ; Δ; Γ ⊢_{A} v_{2} : τ_{i} ⇝^{TAL} v′_{2}

Ψ; Δ; Γ{x:⟨τ_{1}^{φ_{1}}, …, τ_{i−1}^{φ_{i−1}}, τ_{i}^{1}, τ_{i+1}^{φ_{i+1}}, …, τ_{n}^{φ_{n}}⟩} ⊢_{A} let d⃗ in e | L ⇝^{TAL} S, H

Ψ; Δ; Γ ⊢_{A} let x = v_{1}[i] ← v_{2}, d⃗ in e | L ⇝^{TAL}

(mov r, v′_{1} ; mov r′, v′_{2} ; st r[i − 1], r′; S), H ( \begin{matrix}r = r(|Γ| + 1) \\ r′ = r(|Γ| + 2) \\ x ∉ Γ \\ 1 ≤ i ≤ n \end{matrix} )

Figure 25: Term Translation from λ^{A} to TAL Before the resulting TAL code may be run on a real machine, a compiler must perform a final register allocation step to ensure that the TAL code runs with the number of registers supplied by the machine. This may be viewed as a type-preserving optimization within the framework of TAL. A clever register allocator could greatly improve the performance of the output code by choosing registers in order to make moves unnecessary. A practical compiler would want to perform intelligent register allocation as well as other traditional low-level optimizations such as improving instruction selection and scheduling, strength reduction, common subexpression elimination, flowcontrol optimizations, and dead code elimination. Each of these may be implemented as a typepreserving transformation on TAL code using well-known techniques [2].

6.5 TAL Factorial

The factorial computation translated into TAL appears in Figure 26. To obtain the code shown, a few standard optimizations were applied; in particular, a clever (but automatable) register allocation and the removal of redundant moves. If the efficiency of this version is unsatisfactory, a more efficient, tail-recursive version of factorial could be coded in λ^{F}, or a highly optimized version could be hand-coded in TAL:

  l loop:

code[ ]{r1:int,r2:int}. % r1: the product so far, r2: the next number to be multiplied

      bnz r2,l nonzero     % check if done

halt[int] % halt with result in r1

  l nonzero:

code[ ]{r1:int,r2:int}.

mul r1,r1,r2 % multiply next number sub r2,r2,1 % decrement the counter

      jmp l loop
  l fact:

code[ ]{r1:int}. % compute factorial of r1 mov r2,r1 % set up for loop

      mov r1,1
      jmp l loop
with S = mov r1,6; jmp l fact.

7 Compiler Type Correctness

We have presented a compiler for System F which translates programs through a series of four intermediate lambda calculi before finally generating typed assembly language. The full compiler may then be defined by the judgment ⊢_{F} e : τ ⇝ P:

⊢_{F} e : τ ⇝^{cps} e_{cps} ∅; ∅ ⊢_{K} e_{cps} ⇝^{clos} e_{clos} ⊢_{C} e_{clos} ⇝^{hst} P_{hst} ⊢_{H} P_{hst} ⇝^{alloc} P_{alloc} ⊢_{A} P_{alloc} ⇝^{TAL} P
⊢_{F} e : τ ⇝ P

For each translation we have given a type correctness lemma. A corollary of these type correctness lemmas is the type correctness of the entire compiler:

(H, {}, S) where

H =
l fact:
code[ ]{r1:⟨⟩,r2:int,r3:τ_{k}}.
bnz r2,l nonzero

unpack [α,r3],r3 % zero branch: call k (in r3) with 1 ld r4,r3[0] % project k code ld r1,r3[1] % project k environment

mov r2,1

jmp r4 % jump with {r1 = env, r2 = 1}

l nonzero:

code[ ]{r1:⟨⟩,r2:int,r3:τ_{k}}.

sub r4,r2,1                             % n − 1

malloc r5[int, τ_{k}] % create environment for cont in r5 st r5[0],r2 % store n into environment st r5[1],r3 % store k into environment malloc r3[∀[ ].{r1:⟨int^{1}, τ_{k}^{1}⟩,r2:int}, ⟨int^{1}, τ_{k}^{1}⟩] % create cont closure in r3

mov r2,l cont

st r3[0],r2 % store cont code st r3[1],r5 % store environment ⟨n, k⟩

mov r2,r4                               % arg := n − 1

mov r3,pack [⟨int^{1}, τ_{k}^{1}⟩,r3] as τ_{k} % abstract the type of the environment jmp l f % jump to k with {r1 = env, r2 = n − 1, r3 = cont}

l cont:

code[ ]{r1:⟨int^{1}, τ_{k}^{1}⟩,r2:int}. % r2 contains (n − 1)!

ld r3,r1[0]                             % retrieve n
ld r4,r1[1]                             % retrieve k
mul r2,r3,r2                            % n × (n − 1)!
unpack [α,r4],r4                        % unpack k

ld r3,r4[0] % project k code ld r1,r4[1] % project k environment jmp r3 % jump to k with {r1 = env, r2 = n!}

l halt:

code[ ]{r1:⟨⟩,r2:int}.

mov r1,r2

halt[int] % halt with result in r1

and S = malloc r1[ ] % create an empty environment (⟨⟩) malloc r2[ ] % create another empty environment malloc r3[∀[ ].{r1:⟨⟩,r2:int}, ⟨⟩] % create halt closure in r3

mov r4,l halt

st r3[0],r4 % store cont code st r3[1],r2 % store environment ⟨⟩ mov r2,6 % load argument (6) mov r3,pack [⟨⟩,r3] as τ_{k} % abstract the type of the environment jmp l fact % begin fact with {r1 = ⟨⟩, r2 = 6, r3 = haltcont}

and τ_{k} = ∃α.⟨∀[ ].{r1:α,r2:int}^{1}, α^{1}⟩

Figure 26: Typed Assembly Code for Factorial Lemma 7.1 ∅; ∅ ⊢_{F} e : τ if and only if there exists P such that ⊢_{F} e : τ ⇝ P

Lemma 7.2 (Compiler Type Correctness) If ⊢_{F} e : τ ⇝ P then ⊢_{TAL} P

8 Extensions and Practice

We claim that the framework presented here is a practical approach to compilation. To substantiate this claim, we are constructing a compiler called TALC that maps the KML programming language [11] to a variant of the TAL described here, suitably adapted for the Intel x86 family of processors. We have found it straightforward to enrich the target language type system to include support for other type constructors, such as references, higher-order constructors, and recursive types. We omitted discussion of these features here in order to simplify the presentation.

Although this paper describes a CPS-based compiler, we opted to use a stack-based compilation model in the TALC compiler. Space considerations preclude a complete discussion of the details needed to support stacks, but the primary mechanisms are as follows: The size of the stack and the types of its contents are specified by stack types, and code blocks indicate stack types describing the state of the stack they expect. Since code is typically expected to work with stacks of varying size, functions may quantify over stack type variables, resulting in stack polymorphism.

Efficient support for disjoint sums and arrays also requires considerable additions to the type system. For sums, the critical issue is making the projection and testing of tags explicit. In a naive implementation, the connection between a sum and its tag is forgotten once the tag is loaded. For arrays the issue is that the index for a subscript or update operation must be checked to see that it is in bounds. Exposing the bounds check either requires a fixed code sequence, thereby constraining optimization, or else the type system must be strengthened so that some (decidable) fragment of arithmetic can be encoded in the types. Sums may also be implemented with either of the above techniques, or by using abstract types to tie sums to their tags. In the TALC compiler, in order to retain a simple type system and economical typechecking, we have initially opted for fixed code sequences but are exploring the implications of the more complicated type systems.

Finally, since we chose a type-erasure interpretation of polymorphism, adding floats to the language requires a boxing translation. However, recent work by Leroy [24] suggests that it is only important to unbox floats in arrays and within compilation units, which is easily done in our framework.

9 Summary

We have given a compiler from System F to a statically typed assembly language. The type system for the assembly language ensures that source level abstractions such as closures and polymorphic functions are enforced at the machine-code level. Furthermore, the type system does not preclude aggressive low-level optimization, such as register allocation, instruction selection, or instruction scheduling. In fact, programmers concerned with efficiency can hand-code routines in assembly, as long as the resulting code typechecks. Consequently, TAL provides a foundation for highperformance computing in environments where untrusted code must be checked for safety before being executed.

Acknowledgements

We are grateful to Martin Elsman, Úlfar Erlingsson, Dan Grossman, Robert Harper, Jason Hickey, Dexter Kozen, Frederick Smith, Stephanie Weirich, and Steve Zdancewic for their many helpful comments and suggestions.

References

[1] Shail Aditya, Christine Flood, and James Hicks. Garbage collection for strongly-typed languages using run-time type reconstruction. In ACM Conference on Lisp and Functional Programming, pages 12–23, Orlando, June 1994.

[2] Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.

[3] Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992.

[4] Andrew W. Appel and Trevor Jim. Continuation-passing, closure-passing style. In Sixteenth ACM Symposium on Principles of Programming Languages, pages 293–302, Austin, January 1989.

[5] Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In Martin Wirsing, editor, Third International Symposium on Programming Language Implementation and Logic Programming, pages 1–13, New York, August 1991. Springer-Verlag. Volume 528 of Lecture Notes in Computer Science.

[6] Brain Bershad, Stefan Savage, Przemyslaw Pardyak, Emin Sirer, Marc Fiuczynski, David Becker, Craig Chambers, and Susan Eggers. Extensibility, safety and performance in the SPIN operating system. In Fifteenth ACM Symposium on Operating Systems Principles, pages 267–284, Copper Mountain, December 1995.

[7] Lars Birkedal, Nick Rothwell, Mads Tofte, and David N. Turner. The ML Kit (version 1). Technical Report 93/14, Department of Computer Science, University of Copenhagen, 1993.

[8] Lars Birkedal, Mads Tofte, and Magnus Vejlstrup. From region inference to von Neumann machines via region representation inference. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 171–183, St. Petersburg, January 1996.

[9] Hans J. Boehm and Mark Weiser. Garbage collection in an uncooperative environment. Software Practice and Experience, 18(9):807–820, September 1988.

[10] Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172–221, 1991.

[11] Karl Crary. KML Reference Manual. Department of Computer Science, Cornell University, 1996.

[12] Karl Crary. Foundations for the implementation of higher-order subtyping. In ACM SIGPLAN International Conference on Functional Programming, pages 125–135, Amsterdam, June 1997.

[13] Olivier Danvy and Andrzej Filinski. Representing control: a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, December 1992.

[14] Allyn Dimock, Robert Muller, Franklyn Turbak, and J. B. Wells. Strongly typed flow-directed reprsentation transformations. In ACM SIGPLAN International Conference on Functional Programming, pages 85–98, Amsterdam, June 1997.

[15] M. J. Fischer. Lambda calculus schemata. In Proceedings of the ACM Conference on Proving Assertions about Programs, pages 104–109, 1972.

[16] Jean-Yves Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination de coupures dans l’analyse et la théorie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 63–92. North-Holland Publishing Co., 1971.

[17] Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972.

[18] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[19] Robert Harper and Mark Lillibridge. Explicit polymorphism and CPS conversion. In Twentieth ACM Symposium on Principles of Programming Languages, pages 206–219, Charleston, January 1993.

[20] David Kranz, R. Kelsey, J. Rees, P. R. Hudak, J. Philbin, and N. Adams. ORBIT: An optimizing compiler for Scheme. In Proceedings of the ACM SIGPLAN ’86 Symposium on Compiler Construction, pages 219–233, June 1986.

[21] P. J. Landin. The mechanical evaluation of expressions. Computer J., 6(4):308–20, 1964.

[22] John Launchbury and Simon L. Peyton Jones. State in Haskell. LISP and Symbolic Computation, 8(4):293–341, December 1995.

[23] Xavier Leroy. Unboxed objects and polymorphic typing. In Nineteenth ACM Symposium on Principles of Programming Languages, pages 177–188, Albuquerque, January 1992.

[24] Xavier Leroy. The effectiveness of type-based unboxing. In Workshop on Types in Compilation, Amsterdam, June 1997. ACM SIGPLAN. Published as Boston College Computer Science Dept. Technical Report BCCS-97-03.

[25] Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.

[26] Robin Milner, Mads Tofte, Robert Harper, and Dave MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

[27] Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 271–283, St. Petersburg, January 1996.

[28] John C. Mitchell and Gordon D. Plotkin. Abstract types have existential type. ACM Transactions on Progamming Languages and Systems, 10(3):470–502, July 1988.

[29] G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL/ML compiler: Performance and safety through types. In Workshop on Compiler Support for Systems Software, Tucson, February 1996.

[30] Greg Morrisett and Robert Harper. Semantics of memory management for polymorphic languages. In A.D. Gordon and A.M. Pitts, editors, Higher Order Operational Techniques in Semantics, Publications of the Newton Institute. Cambridge University Press, 1997.

[31] Gregory Morrisett. Compiling with Types. PhD thesis, Carnegie Mellon University, 1995. Published as CMU Technical Report CMU-CS-95-226.

[32] George Necula. Proof-carrying code. In Twenty-Fourth ACM Symposium on Principles of Programming Languages, pages 106–119, Paris, 1997.

[33] George Necula and Peter Lee. Safe kernel extensions without run-time checking. In Proceedings of Operating System Design and Implementation, pages 229–243, Seattle, October 1996.

[34] Simon L. Peyton Jones, Cordelia V. Hall, Kevin Hammond, Will Partain, and Philip Wadler. The Glasgow Haskell compiler: a technical overview. In Proc. UK Joint Framework for Information Technology (JFIT) Technical Conference, July 1993.

[35] G. D. Plotkin. Call-by-name, call-by-value, and the lambda calculus. Theoretical Computer Science, 1:125–159, 1975.

[36] John C. Reynolds. Towards a theory of type structure. In Programming Symposium, volume 19 of Lecture Notes in Computer Science, pages 408–425, New York, 1974.

[37] Erik Ruf. Partitioning dataflow analyses using types. In Twenty-Fourth ACM Symposium on Principles of Programming Languages, pages 15–26, Paris, January 1997.

[38] Z. Shao. An overview of the FLINT/ML compiler. In Workshop on Types in Compilation, Amsterdam, June 1997. ACM SIGPLAN. Published as Boston College Computer Science Dept. Technical Report BCCS-97-03.

[39] Zhong Shao. Flexible representation analysis. In ACM SIGPLAN International Conference on Functional Programming, pages 85–98, Amsterdam, June 1997.

[40] Guy L. Steele Jr. Rabbit: A compiler for Scheme. Master’s thesis, MIT, 1978.

[41] D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 181–192, Philadelphia, May 1996.

[42] Mads Tofte. Type inference for polymorphic references. Information and Computation, 89:1–34, November 1990.

[43] Andrew Tolmach. Tag-free garbage collection using explicit type parameters. In ACM Conference on Lisp and Functional Programming, pages 1–11, Orlando, June 1994.

[44] Philip Wadler. Comprehending monads. In ACM Conference on Lisp and Functional Programming, pages 61–78, Nice, June 1990.

[45] Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Programming Concepts and Methods, Sea of Galilee, Israel, April 1990. North Holland. IFIP TC 2 Working Conference.

[46] Philip Wadler. A taste of linear logic. In Mathematical Foundations of Computer Science, volume 711 of LNCS, Gdansk, Poland, August 1993. Springer-Verlag.

[47] Robert Wahbe, Steven Lucco, Thomas Anderson, and Susan Graham. Efficient software-based fault isolation. In Fourteenth ACM Symposium on Operating Systems Principles, pages 203–216, Asheville, December 1993.

[48] Mitchell Wand. Correctness of procedure representations in higher-order assembly language. In S. Brookes, editor, Proceedings Mathematical Foundations of Programming Semantics ’91, volume 598 of Lecture Notes in Computer Science, pages 294–311. Springer-Verlag, 1992.

[49] A. K. Wright. Simple imperative polymorphism. LISP and Symbolic Computation, 8(4), December 1995.

A Soundness of TAL

Lemma A.1 (Context Strengthening) If Δ ⊆ Δ′ then:

1. If Δ ⊢_{TAL} τ type then Δ′ ⊢_{TAL} τ type

2. If Δ ⊢_{TAL} τ_{1} ≤ τ_{2} type then Δ′ ⊢_{TAL} τ_{1} ≤ τ_{2} type. Proof:

Part 1 is immediate by (type). Part 2 is by induction on derivations. □

Lemma A.2 (Subtyping Regularity) If Δ ⊢_{TAL} τ ≤ τ′ type then Δ ⊢_{TAL} τ type and Δ ⊢_{TAL} τ′ type. Proof:

By induction on derivations. □

Lemma A.3 (Heap Extension) If ⊢_{TAL} H : Ψ heap, ∅ ⊢_{TAL} τ type, Ψ{ℓ : τ} ⊢_{TAL} h : τ hval, and ℓ ∉ H then:

1. ⊢_{TAL} Ψ{ℓ : τ} htype

2. ⊢_{TAL} H{ℓ ↦ h} : Ψ{ℓ : τ} heap

3. If Ψ ⊢_{TAL} R : Γ regfile then Ψ{ℓ : τ} ⊢_{TAL} R : Γ regfile

4. If Ψ; Δ; Γ ⊢_{TAL} S then Ψ{ℓ : τ}; Δ; Γ ⊢_{TAL} S

5. If Ψ ⊢_{TAL} h : σ hval then Ψ{ℓ : τ} ⊢_{TAL} h : σ hval

6. If Ψ; Δ ⊢_{TAL} w : σ^{φ} fwval then Ψ{ℓ : τ}; Δ ⊢_{TAL} w : σ^{φ} fwval

7. If Ψ; Δ ⊢_{TAL} w : σ wval then Ψ{ℓ : τ}; Δ ⊢_{TAL} w : σ wval

8. If Ψ; Δ; Γ ⊢_{TAL} v : σ then Ψ{ℓ : τ}; Δ; Γ ⊢_{TAL} v : σ Proof:

Part 1 is immediate by (heap-type). Part 2 follows from parts 1 and 5. Parts 3–8 are by induction on derivations.

□

Lemma A.4 (Heap Update) If ⊢_{TAL} H : Ψ heap, ∅ ⊢_{TAL} τ ≤ Ψ(ℓ) type, and Ψ{ℓ : τ} ⊢_{TAL} h : τ then:

1. ⊢_{TAL} Ψ{ℓ : τ} htype 2. ⊢_{TAL} H{ℓ ↦ h} : Ψ{ℓ : τ} heap

3. If Ψ ⊢_{TAL} R : Γ regfile then Ψ{ℓ : τ} ⊢_{TAL} R : Γ regfile

4. If Ψ; Δ; Γ ⊢_{TAL} S then Ψ{ℓ : τ}; Δ; Γ ⊢_{TAL} S

5. If Ψ ⊢_{TAL} h : σ hval then Ψ{ℓ : τ} ⊢_{TAL} h : σ hval

6. If Ψ; Δ ⊢_{TAL} w : σ^{φ} fwval then Ψ{ℓ : τ}; Δ ⊢_{TAL} w : σ^{φ} fwval

7. If Ψ; Δ ⊢_{TAL} w : σ wval then Ψ{ℓ : τ}; Δ ⊢_{TAL} w : σ wval

8. If Ψ; Δ; Γ ⊢_{TAL} v : σ then Ψ{ℓ : τ}; Δ; Γ ⊢_{TAL} v : σ Proof:

Part 1 is immediate by (heap-type) and Subtyping Regularity. Part 2 follows from parts 1 and 5. Parts 3–8 are by induction on derivations. The only interesting case is the case for the rule (label). The derivation must end:

Δ ⊢_{TAL} σ′ ≤ σ type

Ψ; Δ ⊢_{TAL} ℓ′ : σ wval

(Ψ(ℓ′) = σ′)

If ℓ ≠ ℓ′ then clearly the inference also holds for Ψ{ℓ : τ}. Suppose ℓ = ℓ′. By hypothesis and Context Strengthening, we deduce Δ ⊢_{TAL} τ ≤ σ′ type. Then the conclusion may be proven with the (trans) rule:

Δ ⊢_{TAL} τ ≤ σ′ type Δ ⊢_{TAL} σ′ ≤ σ type
Δ ⊢_{TAL} τ ≤ σ type
Ψ{ℓ : τ}; Δ ⊢_{TAL} ℓ : σ wval

(Ψ{ℓ : τ}(ℓ) = τ)

□

Lemma A.5 (Register File Update) If Ψ ⊢_{TAL} R : Γ regfile and Ψ; ∅ ⊢_{TAL} w : τ wval then Ψ ⊢_{TAL} R{r ↦ w} : Γ{r : τ} regfile. Proof:

Suppose R is {r_{1} ↦ w_{1}, …, r_{n} ↦ w_{n}} and Γ is {r_{1} ↦ τ_{1}, …, r_{m} ↦ τ_{m}} where r may or may not be in {r_{1}, …, r_{n}}. Since Ψ ⊢_{TAL} R : Γ, by the rule (reg) it must be the case that n ≥ m and Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i} wval (for all 1 ≤ i ≤ n and some τ_{m+1}, …, τ_{n}). So certainly for i such that r_{i} ≠ r, Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i} wval, and by hypothesis Ψ; ∅ ⊢_{TAL} w : τ wval so by rule (reg) Ψ ⊢_{TAL} R{r ↦ w} : Γ{r ↦ τ} regfile.

□

Lemma A.6 (Canonical Heap Forms) If Ψ ⊢_{TAL} h : τ hval then:

1. If τ = ∀[α⃗].Γ then:

(a) h = code[α⃗]Γ.S

(b) Ψ; α⃗; Γ ⊢_{TAL} S

2. If τ = ⟨τ_{0}^{φ_{0}}, …, τ_{n−1}^{φ_{n−1}}⟩ then:

(a) h = ⟨w_{0}, …, w_{n−1}⟩

(b) Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i}^{φ_{i}} fwval

Proof:

By inspection. □

Lemma A.7 (Canonical Word Forms) If ⊢_{TAL} H : Ψ heap and Ψ; ∅ ⊢_{TAL} w : τ wval then: 1. If τ = int then w = i.

2. If τ = ∀[β_{1}, …, β_{m}].Γ then:

(a) w = ℓ[σ_{1}, …, σ_{n}]

(b) H(ℓ) = code[α_{1}, …, α_{n}, β_{1}, …, β_{m}]Γ′.S

(c) Γ = Γ′[σ⃗/α⃗]

(d) Ψ; α_{1}, …, α_{n}, β_{1}, …, β_{m}; Γ′ ⊢_{TAL} S

3. If τ = ⟨τ_{0}^{φ_{0}}, …, τ_{n−1}^{φ_{n−1}}⟩ then:

(a) w = ℓ

(b) H(ℓ) = ⟨w_{0}, …, w_{n−1}⟩

(c) Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i}^{φ_{i}} fwval

4. If τ = ∃α.τ then w = pack [τ′, w′] as ∃α.τ and Ψ; ∅ ⊢_{TAL} w′ : τ[τ′/α] wval.

Proof:

1. By inspection.

2. By induction on the derivation of Ψ; ∅ ⊢_{TAL} w : τ wval: The derivation must end with either the (label) or the (tapp-word) rule. Suppose the former. Then w = ℓ, Ψ(ℓ) = τ′ and ∅ ⊢_{TAL} τ′ ≤ ∀[β⃗].Γ type. Inspection of the subtyping rules then reveals that τ′ = ∀[β⃗].Γ. Since ⊢_{TAL} H : Ψ heap, we may deduce that Ψ ⊢_{TAL} H(ℓ) : ∀[β⃗].Γ hval. The conclusion follows by Canonical Heap Forms. Alternatively, suppose the derivation ends with (tapp-word). Then w = w′[σ] and Ψ; ∅ ⊢_{TAL} w′ : ∀[α, β⃗].Γ′ wval with Γ = Γ′[σ/α]. The conclusion follows by induction.

3. The derivation Ψ; ∅ ⊢_{TAL} w : τ wval must be shown by use of the (label) rule. Thus, w = ℓ, Ψ(ℓ) = τ′ and ∅ ⊢_{TAL} τ′ ≤ ⟨τ_{0}^{φ_{0}}, …, τ_{n−1}^{φ_{n−1}}⟩ type. Let us say that φ ≤ φ and 1 ≤ 0.

Then inspection of the subtype rules reveals that τ′ must be of the form ⟨τ_{0}^{φ′_{0}}, …, τ_{n−1}^{φ′_{n−1}}⟩ with φ′_{i} ≤ φ_{i} (for each 0 ≤ i ≤ n − 1). Since ⊢_{TAL} H : Ψ heap, we may deduce that Ψ ⊢_{TAL} H(ℓ) : ⟨τ_{0}^{φ′_{0}}, …, τ_{n−1}^{φ′_{n−1}}⟩ hval. Thus H(ℓ) = ⟨w_{0}, …, w_{n−1}⟩ and Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i}^{φ′_{i}} fwval by Canonical Heap Forms. It remains to show that Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i}^{φ_{i}} fwval for all 0 ≤ i ≤ n − 1. Suppose φ′_{i} = 1 and φ_{i} = 0 (otherwise the conclusion is immediate). Then Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i}^{1} fwval is shown by the (init) rule, which also permits the deduction of Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i}^{0} fwval.

4. By inspection. □

Lemma A.8 (R̂ Typing) If Ψ ⊢_{TAL} R : Γ regfile and Ψ; ∅; Γ ⊢_{TAL} v : τ then Ψ; ∅ ⊢_{TAL} R̂(v) : τ wval.

Proof:

The proof is by induction on the syntax of v. Cases:

v = w: Immediate.

v = r: The only rule that can type v is (reg-val) and this rule requires τ = Γ(r). The only rule that can type R is (reg) and this rule requires Ψ; ∅ ⊢_{TAL} R(r) : τ wval, the conclusion follows since R̂(r) = R(r).

v = v′[σ]: The only rule that can type v is (tapp-val), so τ = ∀[β⃗].Γ′[σ/α] and Ψ; ∅; Γ ⊢_{TAL} v′ : ∀[α, β⃗].Γ′. By induction we deduce Ψ; ∅ ⊢_{TAL} R̂(v′) : ∀[α, β⃗].Γ′ wval, and then the rule (tappword) proves Ψ; ∅ ⊢_{TAL} R̂(v′)[σ] : ∀[β⃗].Γ′[σ/α] wval. The result follows since R̂(v′[σ]) =

R̂(v′)[σ].

v = pack [σ, v′] as ∃α.τ′: The only rule that can type v is (pack-val), so τ = ∃α.τ′ and Ψ; ∅; Γ ⊢_{TAL} v′ : τ′[σ/α]. By induction we deduce Ψ; ∅ ⊢_{TAL} R̂(v′) : τ′[σ/α] wval and then the rule (pack-word) proves Ψ; ∅ ⊢_{TAL} pack [σ, R̂(v′)] as ∃α.τ′ : ∃α.τ′ wval. The result follows since R̂(pack [σ, v′] as ∃α.τ′) = pack [σ, R̂(v′)] as ∃α.τ′.

□

Lemma A.9 (Canonical Forms) If ⊢_{TAL} H : Ψ hval, Ψ ⊢_{TAL} R : Γ regfile, and Ψ; ∅; Γ ⊢_{TAL} v : τ then:

1. If τ = int then R̂(v) = i.

2. If τ = ∀[β_{1}, …, β_{m}].Γ then:

(a) R̂(v) = ℓ[σ_{1}, …, σ_{n}]

(b) H(ℓ) = code[α_{1}, …, α_{n}, β_{1}, …, β_{m}]Γ′.S

(c) Γ = Γ′[σ⃗/α⃗]

(d) Ψ; α_{1}, …, α_{n}, β_{1}, …, β_{m}; Γ′ ⊢_{TAL} S

3. If τ = ⟨τ_{0}^{φ_{0}}, …, τ_{n−1}^{φ_{n−1}}⟩ then:

(a) R̂(v) = ℓ

(b) H(ℓ) = ⟨w_{0}, …, w_{n−1}⟩

(c) Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i}^{φ_{i}} fwval

4. If τ = ∃α.τ then R̂(v) = pack [τ′, w] as ∃α.τ and Ψ; ∅ ⊢_{TAL} w : τ[τ′/α] wval.

Proof:

Immediate from R̂ Typing and Canonical Word Forms.

□

Lemma A.10 (Type Substitution) If β⃗ ⊢_{TAL} τ_{i} type then:

1. If Ψ; α⃗, β⃗; Γ ⊢_{TAL} S then Ψ; β⃗; Γ[τ⃗/α⃗] ⊢_{TAL} S[τ⃗/α⃗]

2. If Ψ; α⃗, β⃗; Γ ⊢_{TAL} v : τ then Ψ; β⃗; Γ[τ⃗/α⃗] ⊢_{TAL} v[τ⃗/α⃗] : τ[τ⃗/α⃗]

3. If Ψ; α⃗, β⃗ ⊢_{TAL} w : τ wval then Ψ; β⃗ ⊢_{TAL} w[τ⃗/α⃗] : τ[τ⃗/α⃗] wval 4. If α⃗, β⃗ ⊢_{TAL} Γ_{1} ≤ Γ_{2} rftype then β⃗ ⊢_{TAL} Γ_{1}[τ⃗/α⃗] ≤ Γ_{2}[τ⃗/α⃗] rftype

5. If α⃗, β⃗ ⊢_{TAL} τ_{1} ≤ τ_{2} type then β⃗ ⊢_{TAL} τ_{1}[τ⃗/α⃗] ≤ τ_{2}[τ⃗/α⃗] type

6. If α⃗, β⃗ ⊢_{TAL} τ ⊢_{TAL} type then β⃗ ⊢_{TAL} τ[τ⃗/α⃗] type Proof:

By induction on derivations. The only interesting case the case for the rule (type):

FTV (τ) ⊆ {α⃗, β⃗}
α⃗, β⃗ ⊢_{TAL} τ type

The hypothesis must also be proven with the rule (type), so FTV (τ_{i}) ⊆ {β⃗}. Consequently:

FTV (τ[τ⃗/α⃗]) ⊆ FTV (τ) \ {α⃗} ∪ (⋃_{i} FTV (τ_{i}))
⊆ {α⃗, β⃗} \ {α⃗} ∪ {β⃗}
= {β⃗}

Hence we may prove β⃗ ⊢_{TAL} τ[τ⃗/α⃗] type using the (type) rule. □

Lemma A.11 (Register File Weakening) If Δ ⊢_{TAL} Γ_{1} ≤ Γ_{2} rftype and Ψ; Δ ⊢_{TAL} R : Γ_{1} regfile then Ψ; Δ ⊢_{TAL} R : Γ_{2} regfile. Proof:

By inspection of the rules (weaken) and (reg). □

Lemma A.12 (Subject Reduction) If ⊢_{TAL} P and P ⟼ P′ then ⊢_{TAL} P′. Proof:

P has the form (H, R, ι; S) or (H, R, jmp v). Let T D be the derivation of ⊢_{TAL} P. Consider the following cases for jmp or ι:

case jmp: T D has the form:

⊢_{TAL} H : Ψ heap Ψ ⊢_{TAL} R : Γ regfile

Ψ; ∅; Γ ⊢_{TAL} v : ∀[ ].Γ′ ∅ ⊢_{TAL} Γ ≤ Γ′ rftype
Ψ; ∅; Γ ⊢_{TAL} jmp v
⊢_{TAL} P

By the operational semantics, P′ = (H, R, S[σ⃗/α⃗]) where R̂(v) = ℓ[σ⃗] and H(ℓ) = code[α⃗]Γ′′.S. Then:

1. ⊢_{TAL} H : Ψ heap is in T D.

2. From ∅ ⊢_{TAL} Γ ≤ Γ′ rftype and Ψ ⊢_{TAL} R : Γ regfile it follows by Register File Weakening that Ψ ⊢_{TAL} R : Γ′ regfile.

3. By Canonical Forms it follows from Ψ; ∅; Γ ⊢_{TAL} v : ∀[ ].Γ′ that Γ′ = Γ′′[σ⃗/α⃗] and Ψ; α⃗; Γ′′ ⊢_{TAL} S. By Type Substitution we conclude Ψ; ∅; Γ′ ⊢_{TAL} S[σ⃗/α⃗]. case add, mul, sub: T D has the form

⊢_{TAL} H : Ψ heap Ψ ⊢_{TAL} R : Γ regfile

Ψ; ∅; Γ ⊢_{TAL} r_{s} : int Ψ; ∅; Γ ⊢_{TAL} v : int
Ψ; ∅; Γ′ ⊢_{TAL} S
Ψ; ∅; Γ ⊢_{TAL} arith_{p} r_{d}, r_{s}, v; S
⊢_{TAL} P

where Γ′ = Γ{r_{d} : int}. By the operational semantics, P′ = (H, R′, S) where R′ = R{r_{d} ↦ R(r_{s}) p R̂(v)}. Then:

1. ⊢_{TAL} H : Ψ heap is in T D.

2. By Canonical Forms it follows that R(r_{s}) and R̂(v) are integer literals, and therefore Ψ; ∅ ⊢_{TAL} R(r_{s}) p R̂(v) wval. We conclude Ψ ⊢_{TAL} R′ : Γ′ regfile by Register File Update.

3. Ψ; ∅; Γ′ ⊢_{TAL} S is in T D.

case bnz: T D has the form:

⊢_{TAL} H : Ψ heap Ψ ⊢_{TAL} R : Γ regfile

Ψ; ∅; Γ ⊢_{TAL} r : int Ψ; ∅; Γ ⊢_{TAL} v : ∀[ ].Γ′
∅ ⊢_{TAL} Γ ≤ Γ′ rftype Ψ; ∅; Γ ⊢_{TAL} S
Ψ; ∅; Γ ⊢_{TAL} bnz r, v; S
⊢_{TAL} P

If R(r) = 0 then P′ = (H, R, S) and ⊢_{TAL} P′ follows since Ψ; ∅; Γ ⊢_{TAL} S is in T D. Otherwise the reasoning is exactly as in the case for jmp.

case ld: T D has the form

⊢_{TAL} H : Ψ heap Ψ ⊢_{TAL} R : Γ regfile

0 ≤ i ≤ n − 1 φ_{i} = 1
Ψ; ∅; Γ ⊢_{TAL} r_{s} : ⟨τ_{0}^{φ_{0}}, …, τ_{n−1}^{φ_{n−1}}⟩
Ψ; ∅; Γ′ ⊢_{TAL} S
Ψ; ∅; Γ ⊢_{TAL} ld r_{d}, r_{s}[i]; S
⊢_{TAL} P

where Γ′ = Γ{r_{d} : τ_{i}}. By the operational semantics, P′ = (H, R′, S) where R′ = R{r_{d} ↦ w_{i}}, R(r_{s}) = ℓ, H(ℓ) = ⟨w_{0}, …, w_{m−1}} and 0 ≤ i < m. Then:

1. ⊢_{TAL} H : Ψ heap is in T D.

2. By Canonical Forms it follows from Ψ; ∅; Γ ⊢_{TAL} r_{s} : ⟨τ_{0}^{φ_{0}}, …, τ_{n−1}^{φ_{n−1}}⟩ that m = n and Ψ; ∅ ⊢_{TAL} w_{j} : τ_{j}^{φ_{j}} fwval for 0 ≤ j < n. Since φ_{i} = 1 it must be the case (by inspection of the (init) rule) that Ψ; ∅ ⊢_{TAL} w_{i} : τ_{i} wval. By Register File we conclude Ψ ⊢_{TAL} R′ : Γ′ regfile.

3. Ψ; ∅; Γ′ ⊢_{TAL} S is in T D.

case malloc: T D has the form

⊢_{TAL} H : Ψ heap Ψ ⊢_{TAL} R : Γ regfile

∅ ⊢_{TAL} τ_{i} type Ψ; ∅; Γ′ ⊢_{TAL} S type
Ψ; ∅; Γ ⊢_{TAL} malloc r_{d}[τ_{1}, …, τ_{n}]; S
⊢_{TAL} P

where σ = ⟨τ_{1}^{0}, …, τ_{n}^{0}⟩, Ψ′ = Ψ{ℓ : σ}, and Γ′ = Γ{r_{d} : σ}. By the operational semantics, P′ = (H′, R′, S) where H′ = H{ℓ ↦ ⟨?τ_{1}, …,?τ_{n}⟩}, R′ = R{r_{d} ↦ ℓ}, and ℓ ∉ H. Then:

1. By the (tuple) and (uninit) rules we may deduce Ψ′ ⊢_{TAL} ⟨?τ_{1}, …,?τ_{n}⟩ hval : σ. By Heap Extension it follows that ⊢_{TAL} H′ : Ψ′ heap.

2. By the (type), (reflex), and (label) rules we may deduce that Ψ′; ∅ ⊢_{TAL} ℓ : σ wval. By Heap Extension we deduce that Ψ′ ⊢_{TAL} R : Γ regfile and it follows by Register File Update that Ψ′ ⊢_{TAL} R′ : Γ′ regfile.

3. By Heap Extension, Ψ′; ∅; Γ′ ⊢_{TAL} S.

case mov: T D has the form

⊢_{TAL} H : Ψ heap Ψ ⊢_{TAL} R : Γ regfile

Ψ; ∅; Γ ⊢_{TAL} v : τ Ψ; ∅; Γ′ ⊢_{TAL} S
Ψ; ∅; Γ ⊢_{TAL} mov r, v; S
⊢_{TAL} P

where Γ′ = Γ{r : τ}. By the operational semantics, P′ = (H, R′, S) where R′ = R{r ↦ R̂(v)}. Then:

1. ⊢_{TAL} H : Ψ heap is in T D.

2. By R̂ Typing it follows from Ψ; ∅; Γ ⊢_{TAL} v : τ that Ψ; ∅ ⊢_{TAL} R̂(v) : τ wval. Using Register File Update we conclude that Ψ ⊢_{TAL} R′ : Γ′ regfile.

3. Ψ; ∅; Γ′ ⊢_{TAL} S is in T D.

case st: T D has the form

⊢_{TAL} H : Ψ heap Ψ ⊢_{TAL} R : Γ regfile

0 ≤ i ≤ n − 1 Ψ; ∅; Γ ⊢_{TAL} r_{d} : σ_{0}
Ψ; ∅; Γ ⊢_{TAL} r_{s} : τ_{i} Ψ; ∅; Γ′ ⊢_{TAL} S
Ψ; ∅; Γ ⊢_{TAL} st r_{d}[i], r_{s}; S
⊢_{TAL} P

where:

σ_{0} = ⟨τ_{0}^{φ_{0}}, …, τ_{n−1}^{φ_{n−1}}⟩
σ_{1} = ⟨τ_{0}^{φ_{0}}, …, τ_{i−1}^{φ_{i−1}}, τ_{i}^{1}, τ_{i+1}^{φ_{i+1}}, …, τ_{n−1}^{φ_{n−1}}⟩
Γ′ = Γ{r_{d} : σ_{1}}

By the operational semantics, P′ = (H′, R, S) where

H′ = H{ℓ ↦ ⟨w_{0}, …, w_{i−1}, R(r_{s}), w_{i+1}, …, w_{m−1}⟩}

and R(r_{d}) = ℓ, H(ℓ) = ⟨w_{0}, …, w_{m}⟩, and 0 ≤ i < m. Then:

1. Since Ψ; ∅; Γ ⊢_{TAL} r_{d} : σ_{0}, it must be the case that Γ(r_{d}) = σ_{0} and thus since Ψ ⊢_{TAL} R : Γ regfile and R(r_{d}) = ℓ we may deduce Ψ; ∅ ⊢_{TAL} ℓ : σ_{0} wval. The latter judgment must be proven with the (label) rule, hence ∅ ⊢_{TAL} σ′_{0} ≤ σ_{0} type where Ψ(ℓ) = σ′_{0}. Note that it follows from Subtyping Regularity and the definition of σ_{0} that ∅ ⊢_{TAL} τ_{j} type for each 0 ≤ j < n. Let us say that φ ≤ φ and 1 ≤ 0. Inspection of the subtyping rules reveals that σ′_{0} must be of the form ⟨τ_{0}^{φ′_{0}}, …, τ_{n−1}^{φ′_{n−1}}⟩ with φ′_{j} ≤ φ_{j}. Let:

σ′_{1} = ⟨τ_{0}^{φ′_{0}}, …, τ_{i−1}^{φ′_{i−1}}, τ_{i}^{1}, τ_{i+1}^{φ′_{i+1}}, …, τ_{n−1}^{φ′_{n−1}}⟩

Then ∅ ⊢_{TAL} σ′_{1} ≤ σ′_{0} type and ∅ ⊢_{TAL} σ′_{1} ≤ σ_{1} type. Since ⊢_{TAL} H : Ψ heap, we may

deduce that m = n and Ψ; ∅ ⊢_{TAL} w_{j} : τ_{j}^{φ′_{j}} fwval for 0 ≤ j < n. Let Ψ′ = Ψ{r_{d} : σ′_{1}}. By

Heap Update it follows that Ψ′; ∅ ⊢_{TAL} w_{j} : τ_{j}^{φ′_{j}} fwval.

Using R̂ Typing and Heap Update, we may deduce that Ψ′; ∅ ⊢_{TAL} R(r_{s}) : τ_{i} wval and, by applying the (init) and (tuple) rules, we may conclude:

Ψ′; ∅ ⊢_{TAL} ⟨w_{0}, …, w_{i−1}, R(r_{s}), w_{i+1}, …, w_{m−1}⟩ : σ′_{1} hval

Hence ⊢_{TAL} H′ : Ψ′ heap by Heap Update.

2. By Heap Update we may deduce Ψ′ ⊢_{TAL} R : Γ. Recall that ∅ ⊢_{TAL} σ′_{1} ≤ σ_{1} type. Thus, Ψ′; ∅ ⊢_{TAL} ℓ : σ_{1} wval, and by Register File Update we may conclude that Ψ′ ⊢_{TAL} R : Γ′ regfile (since R = R{r_{d} ↦ ℓ}).

3. By Heap Update, Ψ′; ∅; Γ′ ⊢_{TAL} S.

case unpack: T D has the form

⊢_{TAL} H : Ψ heap Ψ ⊢_{TAL} R : Γ regfile

Ψ; ∅; Γ ⊢_{TAL} v : ∃α.τ′ Ψ; α; Γ{r:τ′} ⊢_{TAL} S
Ψ; ∅; Γ ⊢_{TAL} unpack[α, r], v; S
⊢_{TAL} P

By the operational semantics, P′ = (H, R′, S′) where R′ = R{r ↦ w}, S′ = S[τ/α] and R̂(v) = pack [τ, w] as ∃α.τ′. Then:

1. ⊢_{TAL} H : Ψ heap is in T D.

2. By Canonical Forms it follows from Ψ; ∅; Γ ⊢_{TAL} v : ∃α.τ′ that Ψ; ∅ ⊢_{TAL} w : τ′[τ/α] wval. Let Γ′ = Γ{r : τ′[τ/α]}. By Register File Update if follows that Ψ ⊢_{TAL} R′ : Γ′ regfile.

3. By Type Substitution it follows from Ψ; α; Γ{r:τ′} ⊢_{TAL} S that Ψ; ∅; Γ′ ⊢_{TAL} S′.

□

Lemma A.13 (Progress) If ⊢_{TAL} P then either there exists P′ such that P ⟼ P′ or P is of the form (H, R{r1 ↦ w}, halt[τ]) (and, moreover, Ψ; ∅ ⊢_{TAL} w : τ wval for some Ψ such that ⊢_{TAL} H : Ψ heap).

Proof:

Suppose P = (H, R, S_{full}). Let T D be the derivation of ⊢_{TAL} P. The proof is by cases on the first instruction of S_{full}.

case halt: T D has the form:

⊢_{TAL} H : Ψ heap Ψ; ∅ ⊢_{TAL} R : Γ regfile

Ψ; ∅; Γ ⊢_{TAL} r1 : τ
Ψ; ∅; Γ ⊢_{TAL} halt[τ]
⊢_{TAL} (H, R, halt[τ])

By R̂ Typing we may deduce that R̂(r1) is defined and Ψ; ∅ ⊢_{TAL} R̂(r1) : τ wval. In other words, R = R′{r1 ↦ w} and Ψ; ∅ ⊢_{TAL} w : τ wval. case add, mul, sub: T D has the form:

⊢_{TAL} H : Ψ heap Ψ; ∅ ⊢_{TAL} R : Γ regfile

Ψ; ∅; Γ ⊢_{TAL} r_{s} : int Ψ; ∅; Γ ⊢_{TAL} v : int ⋯
Ψ; ∅; Γ ⊢_{TAL} arith_{p} r_{d}, r_{s}, v; S
⊢_{TAL} (H, R, S_{full})

By Canonical Forms, R(r_{s}) and R(v) each represent integer literals. Hence P ⟼ (H, R{r_{d} ↦ R(r_{s}) p R̂(v)}, S).

case bnz: T D has the form:

⊢_{TAL} H : Ψ heap Ψ; ∅ ⊢_{TAL} R : Γ regfile

Ψ; ∅; Γ ⊢_{TAL} r : int Ψ; ∅; Γ ⊢_{TAL} v : ∀[ ].Γ′ ⋯
Ψ; ∅; Γ ⊢_{TAL} bnz r, v; S
⊢_{TAL} (H, R, S_{full})

By Canonical Forms, R(r) is an integer literal and R̂(v) = ℓ[σ_{1}, …, σ_{n}] with H(ℓ) = code[α_{1}, …, α_{n}].Γ′′.S′. If R(r) = 0 then P ⟼ (H, R, S). If R(r) ≠ 0 then P ⟼ (H, R, S′[σ⃗/α⃗]).

case jmp: T D has the form:

⊢_{TAL} H : Ψ heap Ψ; ∅ ⊢_{TAL} R : Γ regfile

Ψ; ∅; Γ ⊢_{TAL} v : ∀[ ].Γ′ ⋯
Ψ; ∅; Γ ⊢_{TAL} jmp v; S
⊢_{TAL} (H, R, S_{full})

By Canonical Forms, R̂(v) = ℓ[σ_{1}, …, σ_{n}] with H(ℓ) = code[α_{1}, …, α_{n}].Γ′′.S′. Hence P ⟼ (H, R, S′[σ⃗/α⃗]).

case ld: T D has the form:

⊢_{TAL} H : Ψ heap Ψ; ∅ ⊢_{TAL} R : Γ regfile Ψ; ∅; Γ ⊢_{TAL} r_{s} : ⟨τ_{0}^{φ_{0}}, …, τ_{n−1}^{φ_{n−1}}⟩ ⋯ Ψ; ∅; Γ ⊢_{TAL} ld r_{d}, r_{s}[i]; S (1 ≤ i < n)
⊢_{TAL} (H, R, S_{full})

By Canonical Forms, R(r_{s}) = ℓ with H(ℓ) = ⟨w_{0}, …, w_{n−1}⟩. Hence P ⟼ (H, R{r_{d} ↦ w_{i}}, S).

case malloc: Suppose S_{full} is of the form malloc r[τ_{1}, …, τ_{n}]; S. Then P ⟼ (H{ℓ ↦

⟨?τ_{1}, …,?τ_{n}⟩}, R{r ↦ ℓ, S) for some ℓ ∉ H. case mov: T D has the form:

⊢_{TAL} H : Ψ heap Ψ; ∅ ⊢_{TAL} R : Γ regfile

Ψ; ∅; Γ ⊢_{TAL} v : τ ⋯
Ψ; ∅; Γ ⊢_{TAL} mov r, v; S
⊢_{TAL} (H, R, S_{full})

By R̂ Typing, R̂(v) is defined. Hence P ⟼ (H, R{r ↦ R̂(v), S). case st: T D has the form:

⊢_{TAL} H : Ψ heap Ψ; ∅ ⊢_{TAL} R : Γ regfile Ψ; ∅; Γ ⊢_{TAL} r_{d} : ⟨τ_{0}^{φ_{0}}, …, τ_{n−1}^{φ_{n−1}}⟩ Ψ; ∅; Γ ⊢_{TAL} r_{s} : τ_{i}  ⋯ Ψ; ∅; Γ ⊢_{TAL} st r_{d}[i], r_{s}; S (1 ≤ i < n)
⊢_{TAL} (H, R, S_{full})

By Canonical Forms, R(r_{d}) = ℓ with H(ℓ) = ⟨w_{0}, …, w_{n−1}⟩. By R̂ Typing, R(r_{s}) is defined. Hence P ⟼ (H{ℓ ↦ ⟨w_{0}, …, w_{i−1}, R(r_{s}), w_{i+1}, …, w_{n−1}⟩}, R, S). case unpack: T D has the form:

⊢_{TAL} H : Ψ heap Ψ; ∅ ⊢_{TAL} R : Γ regfile

Ψ; ∅; Γ ⊢_{TAL} v : ∃α.τ ⋯
Ψ; ∅; Γ ⊢_{TAL} unpack[α, r], v; S
⊢_{TAL} (H, R, S_{full})
By Canonical Forms, R̂(v) = pack [τ′, w] as ∃α.τ. Hence P ⟼ (H, R{r ↦ w}, S[τ′/α]).

□