Refinement types for precisely named cache locations
Matthew A. Hammer1 , Joshua Dunfield2 ,
Dimitrios J. Economou1 , and Monal Narasimhamurthy1
1

arXiv:1610.00097v5 [cs.PL] 21 Oct 2017

2

University of Colorado Boulder
Queen’s University (Canada)

Abstract. Many programming language techniques for incremental computation employ programmer-specified names for cached information.
At runtime, each name identifies a “cache location” for a dynamic data
value or a sub-computation; in sum, these cache location choices guide
change propagation and incremental (re)execution.
We call a cache location name precise when it identifies at most one value
or subcomputation; we call all other names imprecise, or ambiguous. At
a minimum, cache location names must be precise to ensure that change
propagation works correctly; yet, reasoning statically about names in
incremental programs remains an open problem.
As a first step, this paper defines and solves the precise name problem, where we verify that incremental programs with explicit names use
them precisely. To do so, we give a refinement type and effect system,
and prove it sound (every well-typed program uses names precisely). We
also demonstrate that this type system is expressive by verifying example programs that compute over efficient representations of incremental
sequences and sets. Beyond verifying these programs, our type system
also describes their dynamic naming strategies, e.g., for library documentation purposes.

1

Introduction

Language-based incremental computation techniques such as self-adjusting computation and Nominal Adapton (Hammer et al. 2015) strive to improve the
asymptotic time complexity of programs using general-purpose incremental computing techniques that combine function call caching, dynamic dependency graphs,
and change propagation (Acar 2005; Acar et al. 2006b,a, 2009; Acar and LeyWild 2009; Hammer and Acar 2008; Hammer et al. 2009; Ley-Wild et al. 2008,
2009; Chen et al. 2012).
In practice, each such system’s cache implementation exposes a programming
model where the incremental algorithm employs explicit names, where each name
identifies a cache location for dynamic data (a dynamic pointer allocation), or a
cache location for dynamic sub-computations (e.g., the arguments, dependencies,
and results of a recursive function call). For an evaluation derivation D, we say
that an allocated pointer name is precise when it has at most one definition in D,

2

and otherwise we say that a name is ambiguous (or imprecise) when it identifies
two or more data structures and/or sub-computations.
This paper defines a verification problem, the precise name problem, for programs that compute with explicit pointer names: prove that for all possible
inputs, in every execution, each name allocated by the program is precise, and
not ambiguous. That is to say, the problem is to verify that every evaluation
derivation D of a well-typed incremental program defines each name uniquely.
Of course, across successive incremental (re-)evaluations of an incremental
program (derivations D1 , D2 , . . .), each name n may be associated with different
values, when and if this content changes incrementally (e.g., first value v1 , then
later, v2 such that v1 6= v2 ). In these situations, name n is still precise exactly
when, in each execution Di , the incremental program only sees a single, unique
value vi at the location named n.
Hence, the goal of this paper is to statically reason about one execution at
a time (not incremental re-executions) and show that dynamically, in each such
execution, each name is used precisely (uniquely). Before outlining our approach
and contributions, we give background on programming with names.
1.1

Background: Incremental computation with names

In practice, incremental programs employ explicit cache location names (1) to
choose cached allocation names deterministically, and (2) to witness dynamic
independence between subproblems, thereby improving incremental reuse.
Deterministic allocation via precise names. The first role of explicit names for
incremental computing concerns deterministic store allocation, which permits us
to give a meaningful definition to cached allocation. To understand this role,
consider these two evaluation rules (each of the judgement form σ; e ⇓ σ 0 ; v) for
reference cell allocation:
`∈
/ dom(σ)
alloc1
σ; ref1 (v) ⇓ σ{` 7→ v}; ref `

n∈
/ dom(σ)
alloc2
σ; ref2 (n, v) ⇓ σ{n 7→ v}; ref n

The left rule is conventional: ref1 allocates a value v at a store location `; because
the program does not determine `, the implementor of this rule has the freedom to
choose ` any way that they wish. Consequently, this program is not deterministic,
and hence, not a function. Because of this fact, it is not immediately obvious
what it means to cache this kind of dynamic allocation using a technique like
function caching (Pugh and Teitelbaum 1989), or techniques based on it. To
address this question, the programmer can determine a name n for the value v,
as in the right rule. The point of this version is to expose the naming choice
directly to the programmer, and their incremental algorithm.
In some systems, the programmer chooses this name n as the hash value
of value v. This naming style is often called “hash-consing”. We refer to it as
structural naming, since by using it, the name of each ref cell reflects the entire

3

structure of that cell’s content.3 By contrast, in a nominal incremental system,
the programmer generally chooses n to be related to the evaluation context of
using v, and often, to be independent of the value v itself, providing dynamic
independence for subcomputations may otherwise be treated as dependent. Notably, since structural names lack any independence with the content that they
name, structural names cannot provide dynamic independence. We give one example of such a naming strategy below, and many more in Sec. 2.
Dynamic independence via names. Programmers of incremental computations
augment ordinary algorithms with names, permitting incremental computing
techniques like memoization and change propagation to exploit dynamic independence in the cached computation.
As a simple illustrative example, consider the left version of rev below, the
recursive program that reverses a list. After being reversed, suppose the input
list to rev undergoes incremental insertions and removals of list elements. To
respond to these input changes, we wish to update the output (the reversed list)
by using the algorithm for rev below, along with general-purpose incremental
computing techniques, including memoization of recursive calls to rev, marked
by the memo keyword.
rev : List -> List -> List
rev l r = match l with
| Nil
⇒ r
| Cons (h , t ) ⇒
memo ( rev ! t ( Cons (h , r )))

Accumulator r consists of (depends
on) the entire list prefix.

rev : List -> List -> List
rev l r = match l with
| Nil
⇒ r
| Cons (n ,h , t ) ⇒
let rr = ref (n , r ) in
memo ( rev ! t ( Cons (h , rr )))

Ref cell rr affords dynamic independence: rr is never accessed by rev.

The function rev reverses a list of Cons cells, using an accumulator r that holds
the reversed prefix of the list. In the Cons case, the function rev calls itself on
the (dereferenced) tail !t, pusing the list element h onto the accumulator r. To
incrementalize the code for rev, we memoize the recursive call to rev, which
involves matching its arguments with those of cached calls.
During incremental (re)executions, we wish to exploit the fact that each
recursive step of rev is, in a sense, independent of the other recursive steps.
However, the left version’s use of memo fails to achieve this effect on its own,
requiring an additional name n and reference cell rr, as shown on the right.
To understand why, consider how change propagation re-evaluates and how
memoization reuses the cached calls to function rev. Specifically, after an input
change, change propagation re-evaluates a step of rev where the input changed.
Next, the accumulator Cons(h,r) contains any incremental changes to head
value h, as well as any changes in the prefix of the input list (now reversed in
the previous accumulator value r). This fact poses a problem for memoization
since such accumulator changes will repeatedly prevent us from memo-matching
3

The structural hashing approach is closely related to Merkle trees, the basis for
revision-control systems like git.

4

the recursive call to rev, which requires that all arguments match that of a prior
execution. Consequently, change propagation will re-evaluate all the calls that
follow the position of an insertion or removal: This change is recorded in the
accumulator, which has changed structurally.
This memoization issue with rev is an example of a general pattern, also
found in the output accumulators of quicksort and quickhull, and more generally,
in many cases when a recursive algorithm allocates and consumes dynamic data
structures. To address this memoization issue, past researchers suggest that we
introduce nominal ref cells into the accumulator, each allocated with a name
associated with their corresponding input Cons cell (Hammer et al. 2015). In
place of “names”, earlier work variously used the terms (allocation) keys (Acar
2005; Hammer and Acar 2008; Acar and Ley-Wild 2009) and indices (Acar et al.
2006b,a), but the core idea is the same.
In this updated (right hand) version, each name n localizes any change to the
accumulator argument r, since the dynamic dependency graph will record the
fact that rev allocates, but never accesses, these reference cells. More precisely,
these reference cells witness that, in fact, the recursive steps of running rev on a
list are independent. In Sec. 3.4, we show that quickhull (for computing convex
hull) has a similar accumulator structure; again, we use names to separate the
subproblems, yet still efficiently accumulate their results.
1.2

Static reasoning for dynamic cache location names

Statically, we wish to reason about incremental programs with explicit names.
At a minimum, cache location names must be precise to ensure that caching and
change propagation work correctly together. Beyond precision, other name-based
considerations, such as a cache eviction policy, are relevant too. In larger systems,
as we build algorithms that compose, we seek a way of statically organizing and
documenting different cache location name choices made throughout (e.g., see
the quick hull examples in Sec. 3.4).
Meanwhile, existing literature lacks static reasoning tools for cache location
names (see Sec. 8 for details). As a first step in this direction, we give a refinement
type and effects system, toured in the next two sections, and defined formally
in Sec. 5. As our examples demonstrate, these (dependent) refinement types
provide a powerful descriptive tool for statically organizing and documenting
choices about cache location names.
Contributions:
– We define the precise name verification problem for programs that use names
to identify (and cache) their dynamic data and computations.
– We present a refinement type and effect system to describe and verify programs that use explicit allocation names.
– To refine the types, we employ separate name and index term languages, for
statically modeling names and name sets, respectively (Sec. 5). The nameset indices were inspired by set-indexed types in the style of DML (Xi and

5

Pfenning 1999); we extend this notion with polymorphism over kinds and
index functions; the latter was inspired by abstract refinement types (Vazou
et al. 2013).
– In Sec. 3, we tour a collections library for sequences and sets. These programs
demonstrate the descriptive power system.
– To validate our approach theoretically, we give a definition of precise effects
for an evaluation derivation D. We prove that for all well-typed programs,
every evaluation derivation D consists of precise effects (Sec. 7).
– Drawing closer to an implementation, we give a bidrectional version of the
type system that we show is sound and complete with respect to our main
type assignment system (Sec. D).

2

Overview of our approach

Our type system statically approximates the name set of each first-class name,
and the write set of each sub-computation. By reasoning about these sets statically, we rule out programs that contain dynamic type errors, enforce precise
names where desired, and provide descriptive affordances to the programmer, so
that she can specify her program’s nominal effects to others (e.g., in the types
of a module signature).
Without a suitable type system, programmer-chosen allocation names can
quickly give rise to imperative state, and unfortunately, to the potential for
unintended errors that undermine the type safety of a program.
Re-allocation at different types:

Re-allocation at the same type:

let r1 = ref (n , (3 ,9))
let r2 = ref (n , 27)

let r1 = ref (n , 0)
let r2 = ref (n , 27)

What if a common name n is used simultaneously for two reference cells of two
different types? Should a program that re-allocates a name at different types
be meaningful? (e.g., see the first program to left, above). We say, “no”, such
programs are not meaningful: They use a name n imprecisely at two different
types, undermining the basic principle of type safety.
On the other hand, suppose a name n is re-allocated at the same type (e.g.,
if r1 and r2 had the same type, as in the second program), we may consider this
behavior meaningful, though imperative. In this case, we want to know that the
program is imperative, and that we should not cache its behavior in contexts
where we expect precise names.
Complementary roles: Editor and Archivist. To distinguish imperative name
allocation from name-precise computation, our type system introduces two roles,
which we term editor and archivist, respectively; specifically, we define the syntax
for roles as r ::= ed | ar. The archivist role (ar) corresponds to computation whose
dependencies we cache, and the editor role (ed) corresponds to computation
that feeds the archivist with input changes, and demands any changed output

6

that is relevant; in short, the editor represents the world outside the cached
computation.
Consider the following typing rules, which approximate our full type system:

Γ ` vn : Nm[X]

Γ `v:A

Γ ` ref(vn , v) : Ref(A)  r(X)

Γ ` e1 : A  ar(X)
Γ, x : A ` e2 : B  ar(Y)
Γ ` (X ⊥ Y) ≡ Z : NmSet

Γ ` e1 : A  ed(X)
Γ, x : A ` e2 : B  ed(Y)
Γ ` (X ∪ Y) ≡ Z : NmSet

Γ ` let(e1 , x.e2 ) : B  ar(Z)

Γ ` let(e1 , x.e2 ) : B  ed(Z)

The rules conclude with the judgement form Γ ` e : A  r(X), mentioning the
written set with the notation r(X), where the set X approximates the set of
written names, and r is the role.
The first rule types a reference cell allocation named by programmer-chosen
value vn , whose type Nm[X] is indexed by an approximate name set X from
which name value vn is drawn; in the rule’s conclusion, this name set X serves
as the allocation’s write set.
The second and third rules give let sequencing: The second rule enforces the
archivist role, where names are precise. The third rule permits the editor role,
where names allocated later may overwrite names allocated earlier. The two rules
each include a premise that judges the equivalence of name set Z (at sort NmSet)
with sets X and Y, which index the write sets of e1 and e2 , respectively.
For names to be precise, as in the archivist (middle) rule, the written sets X
and Y must be disjoint, which we notate as X⊥Y. Otherwise, X and Y may
overlap, permitting e2 to overwrite one or more names also written by e1 , as in
the third rule. Though not shown here, we permit the archivist to nest within
the editor, as a subroutine, but not vice versa.
In the remainder of this paper, we focus on verifying the archivist’s computations, and we temporarily ignore the editor role, for space considerations.
Name functions, higher-order apartness, write scope. Names are not linear resources in most incremental programs. In fact, it is common for precise programs
to consume a name more than once (e.g., see listings for quickhull in Sec. 3.4).
To disambiguate multiple writes of the same name, implementations commonly
employ distinct memo tables, one for each unique function. In this paper, we
employ a more general notion: name functions.
In particular, we define a higher-order account of separation, or apartness (the
term we use throughout) to compose precise programs. Just as apart names n ⊥
m do not overwrite each other (when written, the two singleton write sets are
disjoint), apart name functions f ⊥ g give rise to name spaces that do not
overwrite each other, i.e., f ⊥ g ⇐⇒ ∀x.f x ⊥ g x. That is, f ⊥ g when the
images of f and g are always disjoint name sets, for any preimage.
To streamline programs for common composition patterns, our type system employs a special, ambient name space, the write scope. As illustrated
in Sec. 3, name functions and write scopes naturally permit name-precise subcomputations to compose into larger (name-precise) computations: Just as functions provide the unit of composition for functional programming, (apart) name
functions provide the unit of composition for (precise) naming strategies.

7

3

Examples

In this section, we demonstrate larger example programs and their types, focusing on a collections library of sequences and sets.
3.1

Examples of datatype definitions: Sequences and sets

We present nominal datatype definitions for sequences and finite maps, as first
presented in Hammer et al. (2015), but without types to enforce precision.
We represent sequences as level trees. Unlike lists, level trees permit efficient random editing (Hammer et al. 2015; Headley and Hammer 2016), and
their balanced binary structure is useful for organizing efficient incremental algorithms (Pugh and Teitelbaum 1989). We represent sets and finite maps as
binary hash tries, which we build from these level trees.
Level tree background: A level tree is a binary tree whose internal binary nodes
are each labeled with a level, and whose leaves consist of sequence elements. A
level tree well-formed when every path from the root to a leaf passes through
a sequence of levels that decrease monotonically. Fortunately, it is simple to
pseudo-randomly generate random levels that lead to probabilistically balanced
level trees (Pugh and Teitelbaum 1989). Because they are balanced, level trees
permit efficient persistent edits (insertions, removals) in logarithmic time, and
zipper-based edits can be even be more efficient (Headley and Hammer 2016).
Further, level trees assign sequences of elements (with interposed levels) a single
canonical tree that is history independent, making cache matches more likely.
For nominal level trees, we use names to identify allocations, permitting us
to express incremental insertions or removals in sequences as O(1) re-allocations
(store mutations). By contrast, without names, each insertion or removal from
the input sequence generally requires O(log(N)) fresh pointer allocations, which
generally cascade during change propagation, often giving rise to larger changes
(Hammer et al. 2015).
Sequences as nominal level trees. Below, type Seq[X] refines the “ordinary type”
for sequences Seq; it classifies sequences whose names are drawn from the set X,
and has two constructors for binary nodes and leaves:
SeqBin : ∀X⊥Y⊥Z : NmSet. Nm[X]→Lev→Ref(Seq[Y])→Ref(Seq[Z])→Seq[X⊥Y⊥Z]
SeqLf : ∀X : NmSet.
Vec → Seq[X]

For simplicity here, we focus on monomorphic sequences at base type (a vector
type Vec for vectors of natural numbers); in the appendix, we show refinement
types for polymorphic sequences whose type parameters may be higher-kinded
(parameterized by names, name sets, and name functions).
In the type of constructor SeqBin, the notation X⊥Y⊥Z denotes a set of
names, and it asserts apartness (pair-wise disjointness) among the three sets.
Binary nodes store a natural number level, classified by type Lev, a name, and
two incremental pointers to left and right sub-trees, of types Ref(Seq[Y]) and

8

Ref(Seq[Z]), respectively. The type Nm[X] classifies first-class names drawn
from the set X. In this case, the apartness X ⊥ Y ⊥ Z means that the name
from X at the SeqBin node is distinct from those in its subtrees, whose names
are distinct from one another (name sets Y vs Z). Generally, computations that
consume a data structure assume that names are non-repeating within a sequence
(as enforced by this type); however, computations conventionally reuse input
names to name corresponding constructors in the output, as in the filter,
trie and quickhull examples below.
In the SeqLf case, we store short vectors of elements to capitalize on lowlevel operations that exploit cache coherency. (In empirical experiments, we often choose vectors with one thousand elements). Notably, this leaf constructor
permits any name set X; we find it useful when types over-approximate their
names, e.g., as used in the type for filter below, which generally filters away
some input names, but does not reflect this fact in its output type.
Sets as nominal hash tries. In addition to sequences, we use balanced trees to
represent sets and finite maps. A nominal hash trie uses the hash of an element to
determine a path in a binary tree, whose pointers are named. The type for Set[X]
is nearly the same as that of Seq[X], above; we just omit the level at the binary
nodes:
SetBin : ∀X⊥Y⊥Z : NmSet. Nm[X] → Ref(Set[Y]) → Ref(Set[Z]) → Set[X⊥Y⊥Z]
SetLf : ∀X : NmSet.
Vec → Set[X]

The natural number vectors at the leaves at meant to represent “small” sets of
natural numbers. (In this section, we focused on giving types for sequences and
sets of natural numbers; Sec. A of the supplement describes polymorphic type
definitions).
A collections library. Sec. 3.2 gives simple structurally recursive algorithms over
level trees that we use as subroutines for later implementing quickhull. In Sec.
3.3, we give an incrementally efficient conversion algorithm trie for building
binary hash tries from level trees; it uses nested structural recursion to convert
a binary tree of type Seq[X] into one of type Set[X]. Sec. 3.4 gives two variants
of the divide-and-conquer quickhull algorithm, which only differ in their naming
strategy. In the context of these examples, we illustrate the key patterns for
typing the collections of Hammer et al. (2015), and relate these patterns to the
relevant typing rules of our system.
3.2

Examples of structural recursion: Reducing and filtering sequences

Fig. 1 gives the type and code for max and filter, which compute the maximum
element of the sequence, and filter the sequence by a predicate, respectively. Both
algorithms use structural recursion over the Seq[X] datatype, defined above.
The computation of max is somewhat simpler. In the leaf case (SeqLf), max
uses the auxiliary function vec_max. In the binary case (SeqBin), max performs
two memoized recursive calls, for its left and right sub-trees. We access these
reference cells using !, as in SML/OCaml notation.

9
max : ∀X : NmSet.
Seq[X] → Nat

 λx : Nm. {x·1} ⊥ {x·2} [X]

filter : ∀X : NmSet.
Seq[X] → (Nat → Bool) → Seq[X]

 λx : Nm. {x·1} ⊥ {x·2} [X]

max seq = match seq with
| SeqLf ( vec ) ⇒ vec_max vec
| SeqBin (n ,_ ,l , r ) ⇒
let (_ , ml ) = memo [ n · 1]( max ! l )
let (_ , mr ) = memo [ n · 2]( max ! r )
if ml > mr then ml else mr

filter seq pred = match seq with
| SeqLf ( vec ) ⇒ SeqLf ( vec_filter vec pred )
| SeqBin (n , lev , l , r ) ⇒
let ( rl , sl ) = memo [ n · 1]( filter ! l pred )
let ( rr , sr ) = memo [ n · 2]( filter ! r pred )
match ( is_empty sl , is_empty sr )
| ( false , false ) ⇒ SeqBin (n , lev , rl , rr )
vec_max
: Vec → Nat
| (_ , true ) ⇒ sl
vec_filter : Vec → (Nat → Bool) → Vec
| ( true , _ ) ⇒ sr

Fig. 1. Recursive functions over sequences: Finding the max element, and filtering elements by a predicate.

In our core calculus, named thunks are the unit of function caching. To use
them, we introduce syntactic sugar for memoization, where memo[n·1](· · ·) expands to code that allocates a named thunk (here, named n·1) and demands its
output value: let x = thunk(n·1,· · ·) in forceref(x). The primitive forceref
forces a thunk, and returns a pair consisting of a reference cell representation of
the forced thunk, and its cached value; the reference cell representation of the
thunk is useful in filter, and later examples, but is ignored in max. The code
listing for max uses two instances of memo, with two distinct names, each based
on the name of the binary node n.
A formal structure for names. Our core calculus defines names as binary trees,
n ::= leaf | hhn, nii. In practice, we often want to build names from primitive
data, such as string constants, natural numbers and bit strings; without loss of
generality, we assume embeddings of these types as binary trees. For instance,
we let 1 be shorthand for hhleaf, leafii, the name with one binary node; similarly,
2 stands for hhleaf, hhleaf, leafiiii and 0 for leaf. In the code listing, we use n·1 as
shorthand for hhn, 1ii. More generally, we use n·m as a right-associative shorthand
for name lists of binary nodes, where 1·2·3 represents the name hh1, hh2, 3iiii.
The following deductive reasoning rules help formalize notions of name equivalence and apartness for name terms:
Γ ` M1 ≡ N1 : Nm
Γ ` M2 ≡ N2 : Nm
Γ ` M1 ⊥ N1 : Nm
Γ ` M1 ≡ N : Nm
Γ ` hhM1 , M2 ii
≡ hhN1 , N2 ii : Nm Γ ` hhM1 , M2 ii ⊥ hhN1 , N2 ii : Nm Γ ` hhM1 , M2 ii ⊥ N : Nm

We use the context Γ to store assumptions about equivalence and apartness (e.g.,
from type signatures) and judge pairs of name terms at a common sort Nm. The
first rule says that two binary names are equivalent if their left and right subnames are equivalent. The second rule says that two binary names are apart
(distinct) if their left names are apart. The third rule says that a binary name is
always distinct from a name equivalent to its left sub-name. In the supplement

10

(Sec. F and Sec. G), we give more rules for deductive apartness and equivalence
of name terms and index terms; here and below, we give a few selected examples.
We turn to the type of max given in the listing. For all sets of names X, the
function finds the natural number in a sequence (index by X). The associated
effect (after the ) consists of the following write set:



λx : Nm. {x·1} ⊥ {x·2} [X] ≡
λx : Nm. {x·1}[X] ⊥ λx : Nm. {x·2}[X]
Specifically, this is an index term that consists of mapping a function over a
name set X, and taking the (disjoint) union of these results. Intuitively
(but
S
informally), this term denotes the following set comprehension: x∈X {x·1, x·2}.
That is, the set of all names x in X, appended with either one of name constants 1
and 2. More generally, the index form f[X] employs a name set mapping funcidx
tion f of sort Nm →
NmSet, where index X is a name set and has sort NmSet.
Here, f :≡ λx. {x·1, x·2}.
The following table of rules give equivalence and apartness reasoning (left vs.
right columns) for index function abstraction and application (top vs. bottom
rows); by convention, we use i and j for general indices that may not be name
sets, and use X, Y and Z for name sets.

Γ, a ≡ b : γ1 ` i ≡ j : γ2


Γ, a ≡ b : γ1 ` i ⊥ j : γ2

idx
Γ ` λa. i ≡ λb. j : γ1 →
γ2

idx
Γ ` λa. i ⊥ λb. j : γ1 →
γ2

idx
Γ ` i ≡ j : Nm →
NmSet
Γ ` X ≡ Y : NmSet

idx
Γ ` i ⊥ j : Nm →
NmSet
Γ ` X ≡ Y : NmSet

Γ ` i[X] ≡ j[Y] : NmSet

Γ ` i[X] ⊥ j[Y] : NmSet

To be equivalent, function bodies must be equivalent under the assumption that
their arguments are equivalent; to be apart, their bodies must be apart. To be
equivalent, function applications must have equivalent functions and arguments;
to be apart, the functions must be apart, with the same argument. These application rules are specialized to set comprehensions, using a function from names
to name sets, and a starting name set. An analogous pair of application rules reason about ordinary function application, with arbitrary input and output sorts
(not shown here).
Allocating structurally recursive output. The type and listing for filter is
similar to that of max. The key difference is that filter builds an output
data structure with named reference cells; it returns a filtered sequence, also
of type Seq[X]. Meanwhile, its write set is the same as that of max.
Rather than allocate redundant cells (which we could, but do not), each
reference cell of filtered output arises from the memo shorthand introduced above.
In particular, when the left and right filtered sub-trees are non-empty, filter
introduces a SeqBin code, with two named pointers, rl and rr, the left and right
references introduced by memoizing function calls’ results. This “trick” works
because the output is built via structural recursion, via memoized calls that
are themselves structurally recursive over the input. Below, we nest structural
recursions.

11
trie :
∀X : NmSet.
Seq[X] → Set[X]


join : ∀X⊥Y : NmSet.


c
λx:Nm. (λy:Nm. {x·y})[join(X)]
[X]

trie seq = match seq with
| SeqLf ( vec ) ⇒ trie_lf vec
| SeqBin (n ,_ ,l , r ) ⇒
let ( tl , _ ) = memo [ n · 1]( trie ! l )
let ( tr , _ ) = memo [ n · 2]( trie ! r )
let trie =[ n ] join n tl tr
trie
where:

c
join(X)
:≡ λx:Nm. {x·1} ⊥ {x·2} ∗ [X]

c
Set[X] → Set[Y] → Set[join(X⊥Y)]
c
 join(X⊥Y)
join n l r = match (l , r ) with
| SetLf ( l ) , SetLf ( r ) ⇒ join_vecs n l r
| SetBin (_ ,_ , _ ) , SetLf ( r ) ⇒
join n · 1 l ( split_vec n · 2 r )
| SetLf ( l ) , SetBin (_ ,_ , _ ) ⇒
join n · 1 ( split_vec n · 2 l ) r
| SetBin ( ln , l0 , l1 ) , SetBin ( rn , r0 , r1 ) ⇒
let (_ , j0 ) = memo [ ln · 1]( join ln · 2 l0 r0 )
let (_ , j1 ) = memo [ rn · 1]( join rn · 2 l1 r1 )
SetBin (n , j0 , j1 )

Fig. 2. Nested structural recursion: Converting sequences into maps

3.3

Example of nested structural recursion: Sequences into maps

Fig. 2 defines functions trie and join. The function trie uses structural recursion, following a pattern similar to max and filter, above. However, compared
to max and filter, the body of the SeqBin case for trie is more involved: rather
than compare numbers, or create a single datatype constructor, it invokes join
on the recursive results of calling trie on the left and right sub-sequences. When
a trie represents a set, the function join computes the set union, following an
algorithm inspired by Pugh and Teitelbaum (1989), but augmented with names.
Given two tries with apart name sets X and Y, trie constructs a trie with
d
d is a function over name sets, whose definition we
names join(X⊥Y),
where join
discuss below.
The ambient write scope: a distinguished name space. To disambiguate the
names allocated by the calls to join, the code for trie uses a name space n, with
the notation let trie =[n]e. In particular, this notation controls the ambient
write scope, the name space for allocations that write the store. Informally, it
says to perform the writes of the sub-computation e by first pre-pending the
name n to each allocation name.
To type the ambient write scope, we use a typing judgement form Γ `N e : A
Nm
X that tracks the ambient name space N, a name term of sort Nm →
Nm. (This
idx
arrow sort over names is more restricted than Nm →
NmSet: it only involves
name construction, and lacks set structure.) Consider the following typing rules
for write scopes (left rule) and name function application (right rule):

Γ ` v1 : Nm[X]

Γ ` v2 : A

Γ `M ref(v1 , v2 ) : Ref[M[X]] A  M[X]

idx
Γ ` v : (Nm →
Nm)[N 0 ]
N◦N 0
Γ`
e:AW

Γ `N scope(v, e) : A  W

The left rule uses the name term M to determine the final allocation name
for a reference cell. As indicated by the conclusion’s type and write effect, it

12

computes a name in set M[X], where index term X gives the name set of the
argument. The thunk rule (not shown here) is similar: it uses the ambient write
scope to determine the allocated name.
The right rule extends the ambient write scope N by name function composition with N 0 , for the duration of evaluating a given subterm e. The notation
in the code listing let x =[n](e) is shorthand for let(x, scope(λa. n·a, e).· · ·).
That is, we prepend name n to each written name from evaluating subterm e.
Our collections library commonly uses this shorthand to disambiguate names
that are re-used across sequenced calls, as in the listings for trie, and in quickhull, below.
Types for recursive name sets. Sometimes we need to specify the names of a
set recursively, as in the code listing for join, which is parameterized by an
argument name n. In some recursive calls to join, this name argument “grows”
into n·1 or n·2. In general, each name may grow a variable number of times.
This generality is required: The algorithm for trie allocates a final binary hash
trie whose structure is generally not isomorphic to the initial level tree; it is
generally larger.
To capture these recursive name-growth patterns, we introduce another special variant of index terms, for describing sets that we “grow” inductively by
applying a function zero or more times to an initial set. We use this index form
d from Fig. 2:
to define join
idx
idx
idx
Γ ` i ≡ j : Nm →
NmSet
Γ ` i ⊥ j : Nm →
NmSet
Γ ` i ≡ j : Nm →
NmSet
Γ ` X ≡ Y : NmSet
Γ ` X ⊥ Y : NmSet
Γ ` X ≡ Y : NmSet
Γ ` i∗ [X] ≡ j∗ [Y] : NmSet Γ ` i∗ [X]
Γ ` i∗ [X] ⊥ j∗ [Y] : NmSet
∗
≡ i [j[Y]] ∪ Y : NmSet

The first rule matches that of the non-recursive form. The second rule is unique
to recursive applications; it witnesses one unfolding of the recursion. The final
rule says that two uses of recursive application are apart when the starting sets
and functions are apart.
3.4

Examples of naming divide-and-conquer: Quickhull

Fig. 3 defines two quickhull functions qh1 and qh2. They consist of the same
sequence-processing steps, but use differing naming strategies, and thus exhibit
different caching and change propagation behavior. Each version computes the
furthest point p from the current line ln by using max_pt, which is similar to
max in Fig. 1. This point p defines two additional lines, (ln.0,p) and (p,ln.1),
which quickhull uses to filter the input points before recurring on these new lines.
We use the typing ingredients introduced above to give two naming strategies,
each with distinct cache behavior. To summarize the naming strategies of max_pt
and filter (each uses structural recursion over level trees), we introduce the

c
common shorthand bin[X]
:≡ λx. {x·1, x·2} [X].
The left naming strategy of qh1 uses the identity of the partition lines to
introduce three name spaces (for the calls to max_pt and filter), and three

13
qh1 :
qh2 :
∀X⊥Y⊥Z : NmSet.
∀X⊥Y⊥Z : NmSet.
Line[X] → Seq[Y] → Seq[Z] → Seq[Y⊥Z]
Line[X] → Seq[Y] → Seq[Z] → Seq[Y⊥Z]


d (X)] [X]
d (Y⊥Z)]
 λx:Nm. (λy:Nm. {x·y})[qh
 λy:Nm. {1·y} ⊥ {2·y} ∗ [qh
1
2
qh1 ln
let p
let l
let r
let h
let h
let h
h

pts h =
=[ ln · 1] max_pt ln pts
=[ ln · 2] filter ( ln .0 , p ) pts
=[ ln · 3] filter (p , ln .1) pts
= memo [ ln · 1]( qh1 (p , ln .1) r h )
= push [ ln · 2]( p , h )
= memo [ ln · 3]( qh1 ( ln .0 , p ) l h )

d (X) :≡
qh
1


c
λa. {1·a, 2·a, 3·a} [bin[X]]
⊥ {1, 2, 3}

qh2 ln
let p
let l
let r
let h
let h
let h
h

pts h =
=[3 · 1] max_pt ln pts
=[3 · 2] filter ( ln .0 , p ) pts
=[3 · 3] filter (p , ln .1) pts
= memo [1]([1]( qh2 (p , ln .1) r h ))
= push [2]( p , h )
= memo [3]([2]( qh2 ( ln .0 , p ) l h ))

d (X) :≡
qh
2


c
λa. {3·1·a, 3·2·a, 3·3·a} [bin[X]]
⊥ {1, 2, 3}

Fig. 3. Two naming strategies for quickhull, same algorithmic structure.
Values

v ::= x | () | (v1 , v2 ) | inji v | name n | nmfn M | ref n | thunk n

Terminal exprs. t ::= ret(v) | λx. e
Expressions

e ::= t | split(v, x1 .x2 .e) | case(v, x1 .e1 , x2 .e2 )
| e v | let(e1 , x.e2 ) | thunk(v, e) | force(v) | ref(v, v) | get(v)
| scope(v, e) | vM v
Fig. 4. Syntax of expressions

allocations, for the two calls to qh1, and the output hull point p that is computed
by max_pt. In this case, the library for computational geometry provides the
lines’ names, where we exploit that quickhull does not process the same line
twice. We elide some details in this reasoning, for brevity.
The right version (qh2) ignores the names of lines. Instead, it names everything based on a binary path in the quickhull call graph: The two recursive calls
to qh2 each extend write scope, first with name 1, then with 2.
The two versions are identical, except for having different naming strategies,
and by extension, different cache behavior. We elide the details, but in brief,
the first strategy is better at changes that disrupt and then restore the hull
(inserting and then removing a new hull point) but it also lacks a simple cache
eviction strategy (when to “forget” about work for a line?). By overwriting
earlier computations based on call graph position, the second naming strategy
is cruder, but gives a natural cache eviction strategy.

4

Program Syntax

The examples from the prior section use an informally defined variant of ML,
enriched with a (slightly simplified) variant of our proposed type system. In this
section and the next, we focus on a core calculus for programs and types, and
on making these definitions precise.

14

4.1

Values and Expressions

Fig. 4 gives the grammar of values v and expressions e. We use call-by-pushvalue (CBPV) conventions in this syntax, and in the type system that follows.
There are several reasons for this. First, CBPV can be interpreted as a “neutral”
evaluation order that includes both call-by-value or call-by-name, but prefers
neither in its design. Second, since we make the unit of memoization a thunk,
and CBPV makes explicit the creation of thunks and closures, it exposes exactly
the structure that we extend to a general-purpose abstraction for incremental
computation. In particular, thunks are the means by which we cache results and
track dynamic dependencies.
Values v consist of variables, the unit value, pairs, sums, and several special
forms (described below).
We separate values from expressions, rather than considering values to be a
subset of expressions. Instead, terminal expressions t are a subset of expressions.
A terminal expression t is either ret(v)—the expression that returns the value
v—or a λ. Expressions e include terminal expressions, elimination forms for
pairs, sums, and functions (split, case and e v, respectively); let-binding (which
evaluates e1 to ret(v) and substitutes v for x in e2 ); introduction (thunk) and
elimination (force) forms for thunks; and introduction (ref) and elimination (get)
forms for pointers (reference cells that hold values).
The special forms of values are names name n, name-level functions nmfn M,
references (pointers), and thunks. References and thunks include a name n, which
is the name of the reference or thunk, not the contents of the reference or thunk.
The syntax described above follows that of prior work on Adapton, including
Hammer et al. (2015). We add the notion of a name function, which captures the
idea of a namespace and other simple transformations on names. The construct
scope(v, e) construct controls monadic state for the current name function, composing it with a name function v within the dynamic extent of its subexpression
e. Name function application M v permits programs to compute with names and
name functions that reside within the type indices. Since these name functions
always terminate, they do not affect a program’s termination behavior.
We do not distinguish syntactically between value pointers (for reference
cells) and thunk pointers (for suspended expressions); the store maps pointers
to either of these.
4.2

Names

Figure 5 shows the syntax of literal names, name terms, name term values, and
name term sorts. Literal names m, n are simply binary trees: either an empty
leaf leaf or a branch node hhn1 , n2ii. Name terms M, N consist of literal names
n and branch nodes hhM1 , M2ii, abstraction λa. M and application M(N).
Nm
Name terms are classified by sorts γ: sort Nm for names n, and γ →
γ for
(name term) functions.
The rules for name sorting Γ ` M : γ are straightforward (Figure 6), as are
the rules for name term evaluation M ⇓M V (Figure 7). We write M =β M 0

15
Names
(binary trees)

m, n ::= leaf
| hhn1 , n2 ii

leaf name
binary name composition

Name terms
M, N ::= n | hhM1 , M2 ii
literal names, binary name composition
(STLC+names)
| a | λa. M | M(N) variable, abstraction, application
Name term values

V ::= n | λa. M

Name term sorts

γ ::= Nm
| γ Nm
→γ

name; inhabitants n
name term function; inhabitants λa. M

Typing contexts

Γ ::= · | Γ, a : γ | · · ·

full definition in Figure 9

Fig. 5. Syntax of name terms: a λ-calculus over names, as binary trees

Γ `M:γ
Γ ` n : Nm

Under Γ , name term M has sort γ
(a : γ) ∈ Γ

M-const

Γ `a:γ

Γ, a : γ 0 ` M : γ
Γ ` (λa. M) : (γ 0 Nm
→ γ)

M-abs

M-var

Γ ` M1 : Nm
Γ ` M2 : Nm
Γ ` hhM1 , M2 ii : Nm

→ γ)
Γ ` M : (γ 0 Nm

Γ ` N : γ0

Γ ` M(N) : γ

M-bin

M-app

Fig. 6. Sorting rules for name terms M

when name terms M and M 0 are convertible, that is, applying any series of
β-reductions and/or β-expansions changes one term into the other.

5

Type System

The structure of our type system is inspired by Dependent ML (Xi and Pfenning
1999; Xi 2007). Unlike full dependent typing, DML is separated into a program
level and a less-powerful index level. The classic DML index domain is integers with linear inequalities, making type-checking decidable. Our index domain
includes names, sets of names, and functions over names. Such functions constitute a tiny domain-specific language that is powerful enough to express useful
transformations of names, but preserves decidability of type-checking.
Indices in DML have no direct computational content. For example, when
applying a function on vectors that is indexed by vector length, the length index
is not directly manipulated at run time. However, indices can indirectly reflect
properties of run-time values. The simplest case is that of an indexed singleton
type, such as Int[k]. Here, the ordinary type Int and the index domain of integers
are in one-to-one correspondence; the type Int[3] has one value, the integer 3.
While indexed singletons work well for the classic index domain of integers,
they are less suited to names—at least for our purposes. Unlike integer constraints, where integer literals are common in types—for example, the length
of the empty list is 0—literal names are rare in types. Many of the name constraints we need to express look like “given a value of type A whose name in the

16

M ⇓M V

V ⇓M V

Name term M evaluates to name term value V

teval-value

M1 ⇓M n1

M2 ⇓M n2

hhM1 , M2 ii ⇓M hhn1 , n2 ii

teval-bin

M ⇓M λa. M 0
N ⇓M V
[V/a]M 0 ⇓M V 0
M(N) ⇓M V 0

teval-app

Fig. 7. Evaluation rules for name terms

set X, this function produces a value of type B whose name is in the set f(X)”. A
DML-style system can express such constraints, but the types become verbose:

∀a : Nm. ∀X : NmSet. (a ∈ X) ⊃ A[a] → B[f(a)]
The notation is taken from one of DML’s descendants, Stardust (Dunfield 2007).
The type is read “for all names a and name sets X, such that a ∈ X, given some
A[a] the function returns B[f(a)]”.
We avoid such locutions by indexing single values by name sets, rather than
names. For types of the shape given above, this removes half the quantifiers and
obviates the ∈-constraint attached via ⊃: ∀X : NmSet. A[X] → B[f(X)]. This
type says the same thing as the earlier one, but now the approximations are
expressed within the indexing of A and B. Note that f, a function on names, is
interpreted pointwise: f(X) = {f(N) | N ∈ X}.
(Standard singletons will come in handy for index functions on names, where
one usually needs to know the specific function.)
For aggregate data structures such as lists, indexing by a name set denotes
an overapproximation of the names present. That is, the proper DML type

∀Y : NmSet. ∀X : NmSet. (Y ⊆ X) ⊃ A[Y] → B[f(Y)]
can be expressed by ∀X : NmSet. A[X] → B[f(X)].
Following call-by-push-value (Levy 1999, 2001), we distinguish value types
from computation types. Our computation types will also model effects, such as
the allocation of a thunk with a particular name.
5.1

Index Level

Figure 8 gives the syntax of index expressions and index sorts (which classify
indices). We use several meta-variables for index expressions; by convention, we
use X, Y, Z, R and W only for sets of names—index expressions of sort NmSet.
Name sets. If we give a name to each element of a list, then the entire list
should carry the set of those names. We write {N} for the singleton name set,
∅ for the empty name set, and X ⊥ Y for a union of two sets X and Y that
requires X and Y to be disjoint; this is inspired by the separating conjunction of
separation logic (Reynolds 2002). While disjoint union dominates the types that
we believe programmers need, our effects discipline requires non-disjoint union,
so we include it (X ∪ Y) as well.

17
Index exprs.

Index sorts

i, j, ::= a
X, Y, Z,
| {N}
R, W
|∅|X⊥Y
|X∪Y
| () | (i, i) | prj1 i | prj2 i
| λa. i | i(j)
| M[i] | i[j] | i∗ [j]
γ ::= · · · | NmSet
|1
|γ∗γ
idx
| γ1 →
γ2

index variable
singleton name set
empty set, separating union
union (not necessarily disjoint)
unit, pairing, and projection
function abstraction and application
name set mapping and set building
name set sort
unit index sort; inhabitant ()
product index sort; inhabitants (i, j)
index functions over name sets

Fig. 8. Syntax of indices, name set sort

Variables, pairing, functions. An index i (also written X, Y, . . . when the index
is a set of names) is either an index-level variable a, a name set (described
above: {N}, X ⊥ Y or X ∪ Y), the unit index (), a pair of indices (i1 , i2 ), pair
projection prjb i for b ∈ {1, 2}, an abstraction λa. i, application i(j), or name
term application M[i].
Name terms M are not a syntactic subset of indices i, though name terms
can appear inside indices (for example, singleton name sets {M}). Because name
terms are not a syntactic subset of indices (and name sets are not name terms),
the application form i(j) does not allow us to apply a name term function to a
name set. Thus, we also need name term application M[i], which applies the
name function M to each element of the name set i. The index-level map form
i[j] collects the output sets of function i on the elements of the input set j. The
Kleene star variation i∗ [j] applies the function i zero or more times to each
input element in set j.
Sorts. We use the meta-variable γ to classify indices as well as name terms.
Nm
We inherit the function space →
from the name term sorts (Figure 5). The
sort NmSet (Figure 8) classifies indices that are name sets. The function space
idx
→
classifies functions over indices (e.g., tuples of name sets), not merely name
terms. The unit sort and product sort classify tuples of index expressions.
Most of the sorting rules in Figure 10 are straightforward, but rule ‘sort-sepunion’ includes a premise extract(Γ ) X ⊥ Y : NmSet, which says that X and Y
are apart (disjoint).
Propositions and extraction. Propositions P are conjunctions of atomic propositions i ≡ j : γ and i ⊥ j : γ, which express equivalence and apartness of indices i
and j. For example, {n1 } ⊥ {n2 } : NmSet implies that n1 6= n2 . Propositions are
introduced into Γ via index polymorphism ∀a : γ | P. E, discussed below.
The function extract(Γ ) (Figure 25 in the appendix) looks for propositions
P, which become equivalence and apartness assumptions. It also translates Γ
into the relational context used in the definition of apartness. We give semantic
definitions of equivalence and apartness in the appendix (Definitions 9 and 10).

18
Kinds

K ::= type
| type ⇒ K
|γ⇒K

kind of value types
type argument (binder space)
index argument (binder space)

Propositions

P ::= tt | P and P
|i⊥j:γ
|i≡j:γ

truth and conjunction
index apartness
index equivalence

Effects

 ::= hW; Ri

Value types A, B ::= α | d | unit
|A+B|A×B
| Ref[i] A
| Thk[i] E
| A[i]
|AB
| Nm[i]
| (Nm Nm
→ Nm)[M]

type variables, type constructors, unit
sum, product
named reference cell
named thunk (with effects)
application of type to index
application of type constructor to type
name type (name in name set i)
name function type (singleton)

Computation types C, D ::= F A | A → E liFt, functions
. . . with effects

E ::= C  
effects
| ∀α : K. E
type polymorphism
| (∀a : γ | P. E) index polymorphism

Typing contexts

Γ ::= ·
| Γ, a : γ
| Γ, α : K
| Γ, d : K
| Γ, N : A
| Γ, N : E
| Γ, x : A
| Γ, P

index variable sorting
type variable kinding
type constructor kinding
ref pointer
thunk pointer
value variable
proposition P holds

Fig. 9. Syntax of kinds, effects, and types

5.2

Kinds

We use a simple system of kinds K (Figure 20 in the appendix). Kind type
classifies value types, such as unit and (Thk[i] E).
Kind type ⇒ K classifies type expressions that are parametrized by a type.
Such types are called type constructors in some languages.
Kind γ ⇒ K classifies type expressions parametrized by an index. For example, the Seq type constructor from Section 3 takes a name set, e.g. Seq[X].
Therefore, this (simplified variant of) Seq has kind NmSet ⇒ type. A more general Seq type would also track its pointers (not just its names), and permit any

element type, and would thus have kind: NmSet ⇒ NmSet ⇒ (type ⇒ type)
5.3

Effects

Effects are described by hW; Ri, meaning that the associated code may write
names in W, and read names in R.

19

Γ `i:γ

Under Γ , index i has sort γ

(a : γ) ∈ Γ
Γ `a:γ
Γ ` i : γ1 ∗ γ2
Γ ` prjb i : γb

sort-var

sort-proj

Γ ` X : NmSet
Γ ` Y : NmSet
Γ ` (X ∪ Y) : NmSet

Γ ` () : 1

Γ ` ∅ : NmSet

sort-union

Γ, a : γ1 ` i : γ2
Γ ` (λa. i) : (γ1 → γ2 )
idx

sort-unit

Γ ` i2 : γ2

Γ ` (i1 , i2 ) : (γ1 ∗ γ2 )

sort-empty

Γ ` X : NmSet
Γ ` Y : NmSet

sort-abs

Γ ` i1 : γ1

Γ ` N : Nm
Γ ` {N} : NmSet

extract(Γ )

sort-singleton

X ⊥ Y : NmSet

Γ ` (X ⊥ Y) : NmSet
idx
Γ ` i : γ1 →
γ2

sort-pair

Γ ` j : γ1

Γ ` i(j) : γ2

sort-sep-union

sort-apply

Γ ` M : Nm Nm
→ Nm
Γ ` j : NmSet

idx
idx
Γ ` i : Nm →
NmSet
Γ ` i : Nm →
NmSet
Γ ` j : NmSet
Γ ` j : NmSet
sort-map
sort-build
sort-star
Γ ` M[j] : NmSet
Γ ` i[j] : NmSet
Γ ` i∗ [j] : NmSet

Fig. 10. Sorts statically classify name terms M, and the name indices i that index types

Effect sequencing (Figure 12) is a (meta-level) partial function over a pair of
effects: the judgment Γ ` 1 then 2 = , means that  describes the combination of having effects 1 followed by effects 2 . Sequencing is a partial function
because the effects are only valid when (1) the writes of 1 are disjoint from the
writes of 2 , and (2) the reads of 1 are disjoint from the writes of 2 . Condition
(1) holds when each cell or thunk is not written more than once (and therefore
has a unique value). Condition (2) holds when each cell or thunk is written before
it is read.
Effect coalescing, written “E after ”, combines “clusters” of effects:

C  h{n2 }; ∅i after h{n1 }; ∅i = C  (h{n1 }; ∅i then h{n2 }; ∅i) = C  h{n1 , n2 }; ∅i
Effect subsumption 1  2 holds when the write and read sets of 1 are subsets
of the respective sets of 2 .
5.4

Types

The value types (Figure 9), written A, B, include standard sums + and products
×; a unit type; the type Ref[i] A of references named i containing a value of
type A; the type Thk[i] E of thunks named i whose contents have type E (see
below); the application A[i] of a type to an index; the application A B of a type
A (e.g. a type constructor d) to a type B; the type Nm[i]; and a singleton type
Nm
(Nm →
Nm)[M] where M is a function on names.
As usual in call-by-push-value, computation types C and D include a connective F, which “lifts” value types to computation types: F A is the type of

20

Γ `v:A

Under assumptions Γ , value v has type A

Γ ` () : unit

(x : A) ∈ Γ

unit

Γ `x:A

Γ `n∈X
Γ ` (name n) : Nm[X]
Γ `n∈X

Γ ` (ref n) : (Ref[X] A)

Γ ` v1 : A 1

Γ ` v2 : A2

Γ ` (v1 , v2 ) : (A1 × A2 )

Γ ` Mv : Nm Nm
→ Nm

name

Γ (n) = A

var

Mv = β M

Γ ` (nmfn Mv ) : (Nm → Nm)[M]
Nm

ref

Γ `n∈X

Γ (n) = E

Γ ` (thunk n) : (Thk[X] E)

pair

namefn

thunk

Fig. 11. Value typing

computations that, when run, return a value of type A. (Call-by-push-value
usually has a connective dual to F, written U, that “thUnks” a computation
type into a value type; in our system, Thk plays the role of U.)
Computation types also include functions, written A → E. In standard
CBPV, this would be A → C, not A → E. We separate computation types
alone, written C, from computation types with effects, written E; this decision
is explained in Appendix B.1.
Computation types-with-effects E consist of C  , which is the bare computation type C with effects , as well as universal quantifiers (polymorphism) over
types (∀α : K. E) and indices (∀a : γ | P. E). In the latter quantifier, the proposition P lets us express quantification over disjoint sets of names.
Value typing rules. The typing rules for values (Figure 11) for unit, variables
and pairs are standard. Rule ‘name’ uses index-level entailment to check that the
name n is in the name set X. Rule ‘namefn’ checks that Mv is well-sorted, and
that Mv is convertible to M. Rule ‘ref’ checks that n is in X, and that Γ (n) = A,
that is, the typing n : A appears somewhere in Γ . Rule ‘thunk’ is similar to ‘ref’.
Computation typing rules. Many of the rules that assign computation types
(Figure 12) are standard—for call-by-push-value—with the addition of effects
and the namespace M. The rules ‘split’ and ‘case’ have nothing to do with
namespaces or effects, so they pass M up to their premises, and leave the type E
unchanged. Empty effects are added by rules ‘ret’ and ‘lam’, since both ret and
λ do not read or write anything. The rule ‘let’ uses effect sequencing to combine
the effects of e1 and the let-body e2 . The rule ‘force’ also uses effect sequencing,
to combine the effect of forcing the thunk with the read effect h∅; Xi.
The only rule that modifies the namespace is ‘scope’, which composes the
given namespace N (in the conclusion) with the user’s v = nmfn N 0 in the
second premise (typing e).
5.5

Bidirectional Version

The typing rules in Figures 11 and 12 are declarative: they define what typings are valid, but not how to derive those typings. The rules’ use of names

21

Γ ` (1 then 2 ) = 

Γ ` 1  2

Effect sequencing

extract(Γ ) ` W1 ⊥ W2 extract(Γ ) ` W1 ∪ W2 ≡ W3
extract(Γ ) ` R1 ⊥ W2 extract(Γ ) ` R1 ∪ R2 ≡ R3

Γ ` (X1 ⊥ Z1 ) ≡ Y1 : NmSet
Γ ` (X2 ⊥ Z2 ) ≡ Y2 : NmSet

Γ ` hW1 ; R1 i then hW2 ; R2 i = hW3 ; R3 i

Γ ` (E after ) = E 0

Γ `M e : E

Γ ` hX1 ; X2 i  hY1 ; Y2 i

Effect coalescing

Γ ` (1 then 2 ) = 

Γ ` (C  2 ) after 1 = (C  )

Γ ` (E after ) = E 0
Γ ` (∀α : K. E) after  = (∀α : K. E 0 )
Γ ` (∀a : γ | P. E) after  = (∀a : γ | P. E 0 )

Under Γ , within namespace M, computation e has type-with-effects E
Γ `M e : (C  1 )

Γ ` 1  2

Γ `M e : (C  2 )
Γ ` v : (A1 × A2 )
Γ, x1 : A1 , x2 : A2 `M e : E
Γ`

M

split(v, x1 .x2 .e) : E

Γ`

ret(v) : (F A)  h∅; ∅i

ret

Γ`

Γ, x1 : A1 `M e1 : E
Γ, x2 : A2 `M e2 : E

Γ `M case(v, x1 .e1 , x2 .e2 ) : E
Γ `M e1 : (F A)  1
Γ, x : A `M e2 : (C  2 )
Γ`

Γ, x : A `M e : E

M

eff-subsume

Γ ` v : (A1 + A2 )

split

Γ `v:A
M

Effect subsumption

 lam
(λx. e) : (A → E)  h∅; ∅i

M

case

Γ ` (1 then 2 ) = 

let(e1 , x.e2 ) : (C  )

Γ ` (E after 1 ) = E1

Γ `M e : (A → E)  1
Γ`

M

Γ `v:A

(e v) : E1

let

app

Γ `M e : E
thunk

thunk(v, e) : F (Thk[M[X]] E)  hM[X]; ∅i
Γ ` v : Nm[X]

Γ`

M

Γ ` (h∅; Xi then ) =  0

Γ ` v : Thk[X] (C  )

force

Γ `M force(v) : (C   0 )
Γ ` v1 : Nm[X]
M

Γ`

Γ ` v2 : A

ref(v1 , v2 ) : F (Ref[M[X]] A)  hM[X]; ∅i
Γ ` vM : (Nm Nm
→ Nm)[M]
Γ ` v : Nm[i]

Γ `N (vM v) : F (Nm[M[i]])  h∅; ∅i
Γ, a : γ, P `M t : E
Γ`

M

t : (∀a : γ | P. E)

AllIndexIntro

Γ, α : K `M t : E
Γ`

M

t : (∀α : K. E)

AllIntro

name-app

Γ ` v : Ref[X] A

ref

M

Γ`

get(v) : (F A)  h∅; Xi

Γ ` v : (Nm Nm
→ Nm)[N 0 ]
N◦N 0
Γ`
e : C  hW; Ri
Γ `N scope(v, e) : C  hW; Ri

extract(Γ ) [i/a]P
Γ `M e : (∀a : γ | P. E)
M

Γ`

e : [i/a]E

Γ `M e : (∀α : K. E)
Γ`

Γ `i:γ

M

Fig. 12. Computation typing

scope

AllIndexElim

Γ `A:K

e : [A/α]E

get

AllElim

22
Pointers p, q ::= n
Stores
S ::= ·
| S, p:v
| S, p:e @ M

name constants
empty store
p points to value v
p points to thunk e, run in scope M

Notation: S{p7→v} and S{p7→e@M} extend S at p
when p ∈
/ dom(S)
S{p7→v} and S{p7→e@M} overwrite S at p when p ∈ dom(S)

S1 `M
m e ⇓ S2 ; t

Under store S in namespace M at current node m,
expression e produces new store S2 and result t

1 ◦M2
S1 `M
e ⇓ S2 ; e 0
m
1
S1 `M
m

scope(M2 , e) ⇓ S2 ; e

(M n) ⇓M p
S1 `M
m

M1 ⇓M λa. M2

scope

S

`M
m

S1 {p7→e @ M} = S2

thunk(name n, e) ⇓ S2 ; ret(thunk p)
S(p) = e @ M0
0
S1 `M
e ⇓ S2 ; t
p

S1 `M
m

0

force(thunk p) ⇓ S2 ; t

force

[n/a]M2 ⇓M p

M1 (name n) ⇓ S; ret(name p)
thunk

(M n) ⇓M p
S1 `M
m

S

S1 {p7→v} = S2

ref(name n, v)
⇓ S2 ; ret(ref p)

S(p) = v
`M
m

name-app

get(ref p) ⇓ S; ret(v)

get

S `M
m t ⇓ S; t

ref

term

Fig. 13. Excerpt from the dynamic semantics (see also Figure 18)

and effects annotations means that standard unification-based techniques, like
Damas–Milner inference, are not easily applicable. For example, it is not obvious
when to apply chk-AllIntro, or how to solve unification constraints over names
and name sets.
We therefore formulate bidirectional typing rules that directly give rise to
an algorithm. For space reasons, this system is presented in the supplementary
material (Appendix D). We prove (in Appendix E) that our bidirectional rules
are sound and complete with respect to the type assignment rules in this section:
Soundness (Thms. 2, 4): Given a bidirectional derivation for an annotated
expression e, there exists a type assignment derivation for e without annotations.
Completeness (Thms. 3, 5): Given a type assignment derivation for e without
annotations, there exist two annotated versions of e: one that synthesizes, and
one that checks. (This result is sometimes called annotatability.)

6

Dynamic Semantics

Name terms. Recall Fig. 7 (Sec. 4.2), which gives the dynamics for evaluating name term M to name term value V. Because name terms lack the ability
to perform recursion and pattern-matching, one may expect that they always
terminate. We demonstrate this using a logical relation (Theorem 6).
Program expressions (Figure 13). Stores hold the mutable state that names
dynamically identify. Big-step evaluation for expressions relates an initial and
final store, and the “current scope” and “current node”, to a program and value.

23

We define this dynamic semantics, which closely mirrors prior work, to show that
well-typed evaluations always allocate precisely.
To make this theorem meaningful, the dynamics permits programs to overwrite prior allocations with later ones: if a name is used ambiguously, the evaluation will replace the old store content with the new store content. The rules ref
and thunk either extend or overwrite the store, depending on whether the allocated pointer name is precise or ambiguous, respectively. We prove that, in fact,
well-typed programs always extend (and never overwrite) the store in any single
derivation. (During change propagation, not modeled here, we begin with a store
and dependency graph from a prior run, and even precise programs overwrite
the store/graph, as discussed in Sec. 1.)
While motivated by incremental computation, we are interested in precise
effects here, not change propagation itself. Consequently, this semantics is simpler than the dynamics of prior work. First, the store never caches values from
evaluation, that is, it does not model function caching (memoization). Next, we
do not build the dependency edges required for change propagation. Likewise,
the “current node” is not strictly necessary here, but we include it for illustration. Were we modeling change propagation, rules ref, thunk, get and force
would create dependency edge structure that we omit here. (These edges relate
the current node with the node being observed.)

7

Metatheory: Type Soundness and Precise Effects

In this section, we prove that our type system is sound with respect to evaluation
and that the type system enforces precise effects: We establish that a well-typed,
terminating program produces a terminal computation of the program’s type,
and that the actual dynamic effects are precise (Def. 2). Specifically, we show
that the type system’s static effects soundly approximate this dynamic behavior.
Consequently, sequenced writes never overwrite one another.
We sometimes constrain typing contexts to be store types, which type store
pointers but not program variables; hence, they only type closed values and
programs:
Definition 1 (Store type). We say that Γ is a store typing, written Γ store-type,
when each assumption in Γ has the reference-pointer-type form p : A or the
thunk-pointer-type form p : E.
Definition 2 (Precise effects). The precise effect of an evaluation derived by D,
written D reads R writes W, is defined in Figure 19 in the appendix.
This is a (partial) function over derivations. We call these effects “precise”
since sibling sub-derivations must have disjoint write sets.
Main theorem: We write hW 0 ; R 0 i  hW; Ri to mean that W 0 ⊆ W and R 0 ⊆ R.
For proofs, see Appendix C.

24

Theorem 1 (Subject Reduction).
Nm
If Γ1 store-type and Γ1 ` M : Nm →
Nm and S derives Γ1 `M e : C  hW; Ri
and ` S1 : Γ1 and D derives S1 `M
e
⇓ S2 ; t then
m
there exists Γ2 ⊇ Γ1 such that Γ2 store-type and ` S2 : Γ2 and Γ2 ` t : C  h∅; ∅i
and D reads RD writes WD and hWD ; RD i  hW; Ri.

8

Related Work

DML (Xi and Pfenning 1999; Xi 2007) is an influential system of limited dependent types or indexed types. Inspired by Freeman and Pfenning (1991), who
created a system in which datasort refinements were clearly separated from ordinary types, DML separates the “weak” index level of typing from ordinary
typing; the dynamic semantics ignores the index level.
Motivated in part by the perceived burden of type annotations in DML,
liquid types (Rondon et al. 2008; Vazou et al. 2013) deploy machinery to infer
more types. These systems also provide more flexibility: types are not indexed
by fixed tuples.
To our knowledge, Gifford and Lucassen (1986) were the first to express
effects within (or alongside) types. Since then, a variety of systems with this
power have been developed. A full accounting of this area is beyond the scope
of this paper; for an overview, see Henglein et al. (2005). We briefly discuss a
type system for regions (Tofte and Talpin 1997), in which allocation is central.
Regions organize subsets of data, so that they can be deallocated together. The
type system tracks each block’s region, which in turn requires effects on types:
for example, a function whose effect is to return a block within a given region.
Our type system shares region typing’s emphasis on allocation, but we differ in
how we treat the names of allocated objects. First, names in our system are finegrained, in contrast to giving all the objects in a region the same designation.
Second, names have structure—for example, the names 2·n = hhhhleaf, leafii, nii
and 1·n = hhleaf, nii share the right subtree n—which allows programmers to
deterministically assign names.
Type systems for variable binding and fresh name generation, such as FreshML
(Pitts and Gabbay 2000) and Pure FreshML (Pottier 2007), can express that sets
of names are disjoint. But the names lack internal structure that relates specific
names across disjoint name sets.
Compilers have long used alias analysis to support optimization passes. Brandauer et al. (2015) extend alias analysis with disjointness domains, which can
express local (as well as global) aliasing constraints. Such local constraints are
more fine-grained than classic region systems; our work differs in having a rich
structure on names.
Techniques for general-purpose incremental computation. General-purpose incremental computation techniques provide a general-purpose change propagation
algorithm. In particular, after an initial run of the program, as the input changes

25

dynamically, change propagation provides a provably sound approach for recomputing the affected output (Acar et al. 2006b; Acar and Ley-Wild 2009; Hammer
et al. 2015). Incremental computation can deliver asymptotic speedups for certain algorithms (Acar et al. 2007, 2008; Sümer et al. 2011; Chen et al. 2012).
These incremental computing abstractions exist in many languages (Shankar and
Bodik 2007; Hammer et al. 2009; Acar and Ley-Wild 2009). The type and effect
system proposed here complements past work on self-adjusting computation. In
particular, we expect that variations of the proposed type system can express
and verify the use of names in much of the work cited above.
Imprecise (ambiguous) names in past literature. Some past systems dynamically detect ambiguous names, either forcing the system to fall back to a nondeterministic name choice (Acar et al. 2006b; Hammer and Acar 2008), or to signal an error and halt (Hammer et al. 2015). In scenarios with a non-deterministic
fall-back mechanism, a name ambiguity carries the potential to degrade incremental performance, making it less responsive and asymptotically unpredictable
in general (Acar 2005). To ensure that incremental performance gains are predictable, past work often merely assumes, without enforcement, that names are
precise (Ley-Wild et al. 2009; Çiçek et al. 2015, 2016).

9

Conclusion

We define the precise name verification problem for programs that use names to
identify (and cache) their dynamic data and computations. We present the first
solution to this problem, in the form of a refinement type and effect system.
We use the proposed type system to verify algorithms from an incremental
collections library, and other standard incremental algorithms, such as quickhull.
Drawing closer to an implementation, we derive a bidirectional version of the
type system, and prove that it corresponds to our declarative type system. A
key challenge in implementing the bidirectional system is handling constraints
over names, name terms and name sets; toward this goal, we give decidable,
syntactic rules to guide these checks.

Acknowledgments
We thank Roly Perera and Kyle Headley for their comments and suggestions
on an earlier drafts. This material is based in part upon work supported by a
gift from Mozilla, a gift from Facebook, and support from the National Science
Foundation under grant number CCF-1619282. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s)
and do not necessarily reflect the views of Mozilla, Facebook or the National Science Foundation.

Bibliography

Umut A. Acar. Self-Adjusting Computation. PhD thesis, Department of Computer
Science, Carnegie Mellon University, May 2005.
Umut A. Acar and Ruy Ley-Wild. Self-adjusting computation with Delta ML. In
Advanced Functional Programming. Springer, 2009.
Umut A. Acar, Guy E. Blelloch, Matthias Blume, Robert Harper, and Kanat Tangwongsan. A library for self-adjusting computation. Electronic Notes in Theoretical
Computer Science, 148(2), 2006a.
Umut A. Acar, Guy E. Blelloch, Matthias Blume, and Kanat Tangwongsan. An experimental analysis of self-adjusting computation. In Proceedings of the ACM Conference
on Programming Language Design and Implementation, 2006b.
Umut A. Acar, Alexander Ihler, Ramgopal Mettu, and Özgür Sümer. Adaptive
Bayesian inference. In Neural Information Processing Systems (NIPS), 2007.
Umut A. Acar, Amal Ahmed, and Matthias Blume. Imperative self-adjusting computation. In Proceedings of the 25th Annual ACM Symposium on Principles of
Programming Languages, 2008.
Umut A. Acar, Guy E. Blelloch, Matthias Blume, Robert Harper, and Kanat Tangwongsan. An experimental analysis of self-adjusting computation. TOPLAS, 32(1):
3:1–53, 2009.
Stephan Brandauer, Dave Clarke, and Tobias Wrigstad. Disjointness domains for finegrained aliasing. In OOPSLA, pages 898–916. ACM Press, 2015.
Ezgi Çiçek, Deepak Garg, and Umut A. Acar. Refinement types for incremental computational complexity. In ESOP, 2015.
Ezgi Çiçek, Zoe Paraskevopoulou, and Deepak Garg. A type theory for incremental
computational complexity with control flow changes. In ICFP, 2016.
Yan Chen, Joshua Dunfield, and Umut A. Acar. Type-directed automatic incrementalization. In ACM SIGPLAN Conference on Programming Language Design and
Implementation (PLDI), pages 299–310. ACM Press, 2012.
Joshua Dunfield. A Unified System of Type Refinements. PhD thesis, Carnegie Mellon
University, 2007. CMU-CS-07-129.
Joshua Dunfield and Neelakantan R. Krishnaswami. Complete and easy bidirectional typechecking for higher-rank polymorphism. In ICFP. ACM Press, 2013.
arXiv:1306.6032 [cs.PL].
Joshua Dunfield and Frank Pfenning. Tridirectional typechecking. In Principles of
Programming Languages, pages 281–292. ACM Press, 2004.
Tim Freeman and Frank Pfenning. Refinement types for ML. In Programming Language
Design and Implementation, pages 268–277. ACM Press, 1991.
David K. Gifford and John M. Lucassen. Integrating functional and imperative programming. In ACM Conference on LISP and Functional Programming, pages 28–38.
ACM Press, 1986.
Matthew A. Hammer and Umut A. Acar. Memory management for self-adjusting
computation. In International Symposium on Memory Management, pages 51–60,
2008.
Matthew A. Hammer, Umut A. Acar, and Yan Chen. CEAL: a C-based language
for self-adjusting computation. In ACM SIGPLAN Conference on Programming
Language Design and Implementation, 2009.

27
Matthew A. Hammer, Joshua Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael Hicks, and David Van Horn. Incremental computation with names. In
OOPSLA, pages 748–766. ACM Press, 2015.
Kyle Headley and Matthew A. Hammer. Simple persistent sequences. In Trends in
Functional Programming, 2016.
Fritz Henglein, Henning Makholm, and Henning Niss. Effect types and region-based
memory management. In B. C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 3, pages 87–135. MIT Press, 2005.
Paul Blain Levy. Call-by-push-value: A subsuming paradigm. In Typed Lambda Calculi
and Applications, pages 228–243. Springer, 1999.
Paul Blain Levy. Call-By-Push-Value. PhD thesis, Queen Mary and Westfield College,
University of London, 2001.
Ruy Ley-Wild, Matthew Fluet, and Umut A. Acar. Compiling self-adjusting programs
with continuations. In ICFP, 2008.
Ruy Ley-Wild, Umut A. Acar, and Matthew Fluet. A cost semantics for self-adjusting
computation. In Principles of Programming Languages, 2009.
Benjamin C. Pierce and David N. Turner. Local type inference. ACM Trans. Prog.
Lang. Syst., 22:1–44, 2000.
Andrew M. Pitts and Murdoch J. Gabbay. A metalanguage for programming with
bound names modulo renaming. In Mathematics of Program Construction. Springer,
2000.
François Pottier. Static name control for FreshML. In Logic in Computer Science,
pages 356–365, 2007.
William Pugh and Tim Teitelbaum. Incremental computation via function caching. In
POPL, 1989.
John C. Reynolds. Separation logic: A logic for shared mutable data structures. In
Logic in Computer Science, pages 55–74, 2002. URL http://www.cs.cmu.edu/~jcr/
seplogic.pdf.
Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala. Liquid types. In Programming
Language Design and Implementation, pages 159–169, 2008.
Ajeet Shankar and Rastislav Bodik. DITTO: Automatic incrementalization of data
structure invariant checks (in Java). In Programming Language Design and Implementation, 2007.
Özgür Sümer, Umut A. Acar, Alexander Ihler, and Ramgopal Mettu. Adaptive exact
inference in graphical models. Journal of Machine Learning, 8:180–186, 2011.
Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Information
and Computation, 132(2):109–176, 1997.
Niki Vazou, Patrick M. Rondon, and Ranjit Jhala. Abstract refinement types. In
European Symp. on Programming, pages 209–228, Berlin Heidelberg, 2013. Springer.
Hongwei Xi. Dependent ML: An approach to practical programming with dependent
types. J. Functional Programming, 17(2):215–286, 2007.
Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In
Principles of Programming Languages, pages 214–227. ACM Press, 1999.

28

A

Programming Examples: Lists, polymorphism

Through self-contained running examples that define and compute over lists, we
give a an overview of our type system. We work towards showing examples of
datatypes, and datatype polymorphism in our proposed system, including how
to define and use abstract types that contain type parameters. Specifically, we
show how to define polymorphic lists that can be instantiated appropriately to
define lists of lists of integers.
We begin with a type for incremental lists of integers. We use this list type
to write list_map. We show how this code, and in particular its use of names,
induces a dependence graph with names that derive from the input list. In particular, we explain two connected activities: (1) augmenting functional programs
to name data and computations, and (2) generalizing these naming strategies
to write composable library functions. Toward the latter goal, we show how to
generalize lists of integers to lists of other structures that may contain names,
such as other (sub)-lists.
In support of creating composable incremental computing libraries, we consider two composition problems, and illustrate how Typed Adapton introduces
additional type-level affordances to overcome them:
– Names are not linear resources: It is natural and common to consume a name
more than once within a computation.4 To disambiguate multiple writes of
the same name, we introduce name functions that permit programmers to
create distinct dynamic scopes. To streamline programs, Typed Adapton
employs a scope monad to capture this dynamic structure.
– Naive type polymorphism ignores how names relate between a structure
(e.g., a list of lists) and the structures that it contains (e.g., the sub-lists
of the outer list). To describe and enforce name-based relationships generically, we parameterize generic types with index-transforming functions. In
turn, these index functions enforce client-chosen invariants that relate the
type indices of sub- and super-structures, which may involve arbitrary name
sets. For instance, we can write one definition of polymorphic lists, and as
clients, instantiate this definition twice to define lists of lists which hold
integers.
A.1

Lists of integers, with names

The type below defines incremental lists of integers, List[X; Y] Int. This type has
two conventional constructors, Nil and Cons, as well as two additional constructors that use the two type indices X and Y. Each index has name set sort NmSet,
which classifies indices that are sets of names.
The Name constructor permits names from set X1 to appear in the list sequence; it creates a Cons-cell-like pair holding a first-class name from X1 (of
4

As anecdotal evidence, consider that functional programs commonly exploit sharing in data structures and algorithms, and often do not adhere to a linear typing
discipline. We still wish to name these computation patterns and data structures.

29

type Nm[X1 ]), and the rest of the sequence, whose names are from X2 . The Ref
constructor permits injecting reference cells holding lists into the list type; these
pointers’ names are drawn from set Y = (Y1 ⊥ Y2 ), the disjoint union of the
possible pointer names Y1 for the head reference cell, and the pointer names Y2
contained in this cell’s list.
Nil
: ∀X, Y : NmSet.
unit
→ List[X; Y] Int
Cons : ∀X, Y : NmSet.
Int →
List[X; Y] Int → List[X; Y] Int
Name : ∀X1 ⊥X2 , Y : NmSet. Nm[X1 ] → List[X2 ; Y] Int → List[X1 ⊥ X2 ; Y] Int
Ref : ∀X, Y1 ⊥Y2 : NmSet. Ref[Y1 ] (List[X; Y2 ] Int) → List[X; Y1 ⊥ Y2 ] Int
For both of these latter forms, the constructor’s types enforce that each name
(or pointer name) in the list is disjoint from those in the remainder of the list.
For instance, when quantifying over these sets, we write X1 ⊥ X2 to impose
the constraint that X1 be disjoint from X2 , and similarly for Y1 ⊥ Y2 ; However,
for the Name constructor, the names in X1 and pointer names in Y may overlap
(or even coincide). These disjointness constraints consist of syntactic sugar that
we expand in Sec. 5. The Nil constructor creates an empty sequence with any
pointer or name type sets in its resulting type, since, for practical reasons, we
find it helpful to permit type indices to over-approximate name sets.
We distinguish two roles of names: unallocated names, which are unassociated
with content of any type, and which need only be locally unique (e.g., unique
to a list or other data structure), and allocated names, which dynamically name
content of some fixed type and must be globally unique; they each identify a
pointer allocated in the store.
In the Name(n,t) form, the name n is unallocated, and can be used to allocate
a reference or thunk of any type. In the Ref(r) form, by contrast, we have a
reference cell r that consists of a pointer name whose type is parameterized by
the type of the content it names, in this case an integer list.
The scope s distinguishes namespaces, and is explained in further detail below; intuitively, name funcion s translates a locally unique name (unique to the
list) into a globally unique name (unique to global program evaluation).
A.2

Mapping a list of integers, with names

Fig. 14 (left listing) lists the type, effect and code for list_map0, which consumes
the list type defined above, but does not allocate any references or thunks. We
include it here for illustrative purposes, as preparation for further examples. The
type signature includes abstract name sets X and Y, for the names and named
pointers of the input list l. The resulting list type is indexed by the name
set X and the empty pointer set ∅ since the output contains the same names
as the input (all drawn from X), but does contain any pointers. The function’s
effect, written as h∅; Yi, indicates that the code writes no names, but reads the
pointers Y from the input list l.
Turning to the program text for list_map0, the Nil and Cons cases are
entirely conventional: They return Nil and apply f to the head of each Cons

30

cell, respectively. The Name and Ref cases handle unallocated names and (allocated) pointers in the list; both are simple recursive cases. In the Name case,
list_map0 maps the input name into corresponding position of the output list
and recurs. In the Ref case, list_map0 uses get to observe the content of the
reference cell holding the remainder of the input, and recurs on this input list.
The right listing gives list_map1, whose code and behavior is identical to
list_map0 on the left, except for in the Name case, where the right version
allocates a reference cell to hold the output list, and it allocates (and forces)
a thunk to memoize the recursive call. (The shorthand memo(e1 ,e2 ) expands
into force(thunk(e1 ,e2 ))). To name these allocations, list_map1 uses the
input list’s name n for the reference cell and a distinct name for the thunk,
(n·1) :≡ hhn, leafii 6= n. Critically, the name n·1 is distinct from both n and any
name that is distinct from n, including the other names in the list. That is, for
all m, we have that (n ⊥ m) ⇒ (n ⊥ n·1 ⊥ m ⊥ m·1), meaning that the four
elements in the consequent are pairwise distinct. Generalizing further, we can
use this pattern to systematically add memoization and reference cells to any
structurally recursive algorithm that includes an analog of this Name case. We
show examples of such algorithms, below.
Comparing its type with list_map0, the returned list type of list_map1
now contains names from X (as before) and pointers from ?(X). The effect is also
affected: the written name set is now ?(X ⊥ X·1), not ∅. These sets refer to the
names written in the revised Name case, mapped by the current monadic scope,
which we denote with the notation ?(−); recall that the scope is a dynamically
specified name-transforming function that we apply to each written name, in this
case drawn from X ⊥ X·1. Further, we use shorthand X·1 to informally mean
“the names of set X, mapped by the function λa. hha, leafii”; in Sec. 5, we make
the syntax for name sets, type indices and effects precise.
A.3

Names identify nodes in a dynamic dependency graph

Suppose that we execute list_map1 on an input list with two integers, two
names a and b, and two reference cells p and q, as shown in the left of Fig. 14.
Bold boxes denote reference cells in the input and output lists, and bold circles
denote memoized thunks that compute with them. Each bold object (thunk or
reference) is named precisely. The two thunks, shown as bold circles named by
a·1 and b·1, follow a similar pattern: each has outgoing edges to the reference
that they dereference (northeast, to p and q, respectively), the recursive thunk
that they force, if any (due west, to b·1 for a·1, and none for b·1), and the
reference that they name and allocate (southeast, to a and b, respectively).
The benefit of using names stems from the nominal indirection that they
afford. Operationally, imperative O(1) changes to the input structure can be
reflected into the output with only O(1) changes to its named content. Further,
for the memoized thunks, the names also provide a primitive form of cache
eviction: Memoized results are overwritten when names are re-associated with
new content.

31
list_map0 : ∀X, Y : NmSet.
(Int → Int) → (List [X; Y] Int) →

list_map1 : ∀X, Y : NmSet.
(Int → Int) → (List[X; Y] Int) →

(List [X; ∅] Int)

(List[X; ?(X) ] Int)

h∅; Yi

h ?(X⊥X·1) ; Yi

list_map1 = λf . fix rec . λl .
list_map0 = λf . fix rec . λl .
match l with
match l with
Nil
⇒ Nil
Nil
⇒ Nil
Cons (h , t ) ⇒ Cons ( f h , rec t )
Cons (h , t ) ⇒ Cons ( f h , rec t )
Name (n , t )
Name (n , t ) ⇒ Name (n ,
rec t )
⇒ Name (n ,
Ref ( ref (n , memo ( n·1 ,
rec t ))))
Ref ( r )
⇒ rec ( get r )
Ref ( r )
⇒ rec ( get r )
Fig. 14. list_map0 (left) and list_map1 (right) consist of the standard algorithm to
map a list of integers l using a given integer function f, augmented with additional
cases for Ref and Name. The left version performs no allocations; the right version uses
names from the input list to name reference cells and recursive calls.

A.4

Scopes distinguish distinct sub-computations

Programs commonly disambiguate two uses of the same name by using two
different write scopes. Specifically, the write scope monad implicitly threads a
name function through the computation, applying it to each name that the
computation allocates. Conceptually, the write scope at the outermost layer
of the computation is the identity name function. As the computation enters
subtrees of the dynamic call tree, the write scope monad nests the write scope
by composing name functions.
let map_pair l =
let xs = scope s1 [ list_map1 f l ]
let ys = scope s2 [ list_map1 g l ]
( xs , ys )
let out = memo (1, map_pair inp )
For instance, consider two uses of map, with two different element-mapping
functions f and g. This code uses disjoint write scopes s1 ⊥ s2 to map an
input list inp twice within a single incremental program to produce a pair of
distinct output lists out that each depend on the common input list inp. To make
the example concrete, suppose that s1 and s2 prepend the name constants 1
and 2 on to their name argument, respectively. This program gives rise to the
dependence graph shown in Fig. 14 (right side). This diagram illustrates how the
two sub-computations of list_map1 share the input list inp: Each of its reference
cells has two incoming get edges. (Recall, names are not linear resources, so
this is not problematic). To distinguish these write scopes, the distinct name
functions hh1, −ii and hh2, −ii disambiguate the name of each reference cell and

32
Name
inp =

Name
inp =

a

thunk,
force
out =

p

Cons
1

a•1

a

Ref

get
ref

Name

Ref

b

thunk; force

Cons Nil
2

b•1

a
f1

q

get
ref

thunk,
force

/

1

b
f2

/

get
ref

Cons

Name

a

get
ref

1•
b•1

thunk; force
f1

2•
a•1

Ref

Cons Nil

get
ref

2•
b•1

thunk; force

get
ref

2

/

f2

/

g2

/

1•b

b

2•a
g1

q

b

1•a

a

1

out =

Ref

1
1•
a•1

2

b

p

a

2•b

b

Fig. 15. Left: The dependence graph produced by evaluating function list_map1
on inp, a two-integer, two-name input list, shown in the two upper blue regions of
the figure. Its names are drawn from set X = {a, b, . . .}, and its pointer names are
drawn from the set Y = {p, q, . . .}. The two purple sections consist of allocated dependence graph nodes that depend on the input list: cell a, thunk a·1, cell b, and thunk b·1.
Right: The dependence graph produced by evaluating map_pair on the same input list,
in two different scopes: 1 and 2. The scopes give rise to precise names for the output
lists and their associated computations.

thunk for list_map1 (e.g., compare the allocated names of the left-hand and
right-hand versions of the figure).
A.5

Polymorphic lists, with names

Above, we considered lists of integers. Now, suppose the archivist wishes to
employ lists of other data structures, such as lists of lists. For instance, past
literature commonly implements incremental mergesort using functions over lists
of lists. First, consider what we call naive type polymorphism, where we replace
each instance of “Int” in type of integer lists (List[X; Y] Int) with the universally
quantified type variable α:
Nil

: ∀α : type. ∀X, Y : NmSet.

Cons : ∀α : type. ∀X, Y : NmSet.

1
α →

→ List[X; Y] α

List[X; Y] α → List[X; Y] α

Name : ∀α : type. ∀X1 ⊥X2 , Y : NmSet. Nm[X1 ] → List[X2 ; Y] α → List[X1 ⊥ X2 ; Y] α
Ref

: ∀α : type. ∀X, Y1 ⊥Y2 : NmSet. Ref[Y1 ] (List[X; Y2 ] α ) → List[X; Y1 ⊥ Y2 ] α

As we demonstrate, naively parameterizing lists by α does not afford enough
invariants to verify all the programs that we wish to author. For instance, suppose the archivist wishes to express the list transformation list_join that appends the sub-lists of a list of lists; in the Cons case, it uses auxiliary function list_append to append the sublist at the head with the remainder of the
sublists’ elements in the (flattened) tail.
Fig. 16 lists the code for these standard list algorithms, as well as types for
each. As with list_map0, we initially consider versions that do not allocate,
for simplicity; later, we can augment the algorithms with named allocations in
the same fashion that we systematically transformed list_map0 into list_map1.
The code for list_append0 checks against the listed type, with reasoning similar
to that of list_map0; it does not involve lists of lists, only lists of integers. As

33
X
?
list_append0 :
list_join0 :
∀X1 ⊥X2 , Y1 ⊥Y2 : NmSet.
∀X1 ⊥X2 , Y1 ⊥Y2 : NmSet.


List[X1 ; Y1 ] Int 
List[X1 ; Y1 ] (List[X2; Y2 ] Int)
→ List[X2 ; Y2 ] Int
→ List[X1 ⊥X2 ; ∅] Int

→ List[X1 ⊥X2 ; Y2 ] Int
 h∅, Y1 ⊥Y2 i
 h∅, Y1 i
list_append0 = fix rec . λl . λr . list_join0 = fix rec . λl .
match l with
match l with
Nil
⇒r
Nil
⇒ Nil
Cons (h , t ) ⇒ let t ’ = rec t r
Cons (h , t ) ⇒ let t ’ = rec t
Cons (h , t ’)
list_append0 h t ’
Name (n , t ) ⇒ Name (n , rec t )
Name (n , t ) ⇒ Name (n , rec t )
Ref ( r )
⇒ rec ( get r )
Ref ( r )
⇒ rec ( get r )
Fig. 16. Function list_append0 copies one list l, replacing its Nil terminal with a
second list r. Function list_join0 appends the sub-lists of a list of lists. The naive
polymorphic list type for list_join0 is insufficient to type-check the Cons case of its
body.

we explain below, the code for list_join0 does not check against the listed
type: The listed type uses polymorphism naively with respect to name sets. To
overcome this problem, we need to change the refinement type for Cons. To see
why, first consider checking the body against the listed type.
Consider the Cons case of list_join0, whose code is standard; in the case
of a sublist h, we append this sublist to the result of flattening the rest of the
input list of lists. Critically, this step involves reasoning about the relationship
between three structures, each involving a set of names:
– The head h of the list of lists l, with names drawn from X2 (Inner list h has
type List[X2 ; Y2 ] Int),
– The tail t of the list of lists l, with outer list names drawn from X1 and
inner list names from X2 , and
– The flattened tail t’ of of tail t, with names drawn from X1 ⊥ X2 .
In particular, to prove that the use of list_append0 h t’ is well-typed, we wish
to argue that head h (drawn from X2 ) has names that are distinct from those
in the flattened list t’ (drawn from X1 ⊥ X2 ). However, the naive polymorphic
list type places no constraints on names in different sub-lists: It merely says that
their names are all drawn from X2 , not that each distinct sub-list uses a distinct,
non-overlapping subset of X2 .
Recall the type of Cons given above:
∀α : type. ∀X, Y : NmSet. α → (List[X; Y] α) → (List[X; Y] α)
In particular, we want the type for Cons to enforce a relationship of disjointness
between the name sets of the new element and the existing elements in the list,
which is does not. Further, as written, each occurrence of α must be the same,

34

and thus, must over-approximate name sets. Instead, the following types for
Cons will permit list_join to type-check; we discuss them in turn:
Lists of lists of integers:
Cons :
∀X⊥X1 ⊥X2 : NmSet.
∀Y⊥Y1 ⊥Y2 : NmSet.

Lists of α (type α has kind γ → type):
Cons : ∀X, Y : NmSet. ∀i, j : γ.
∀k1 ≡ f i j : γ.
∀k2 ≡ g X Y k1 : NmSet × NmSet.

(List[X1 ; Y1 ] Int)
→ (List[X; Y] (List[X2 ; Y2 ] Int))
→ List[X⊥X1 ⊥X2 ; Y⊥Y1 ⊥Y2 ]
(List[X1 ⊥X2 ; Y1 ⊥Y2 ] Int)

α[i]
→ (List[X; Y] (α[j]))
→ (List[k2 ] (α[k1 ]))

First consider the type on the left, which is specific to lists of lists of integers.
In particular, this type enforces that the sublists’ names are disjoint from one
another, and from the names of the outer list. Consequently, in the Cons case
of list_join, we can justify the recursive call, since the outer and inner lists
have distinct names; and, we can justify the call to list_append, since the names
of each inner list are distinct from those of other inner lists.
Instead of writing a new version of Cons for every list element type, we want
to capture this pattern, and others, generically. The second (rightmost) type of
Cons is generic in type α, but unlike the naive polymorphic type, this version
permits the indices of the type parameter α to vary across occurrences (i versus
j), while enforcing user-defined constraints over these index occurrences (index
function f), and between these element indices and the indices of the list (index
function g). In particular, the client of this generic list chooses a type α, with
some index sort γ, and they choose index functions f and g:
idx
idx
f :γ→
γ→
γ
idx
idx
idx
g : NmSet → NmSet →
γ→
(NmSet × NmSet)

As described by its sort, index function f forms an element index from two
elements’ indices (each of sort γ). Likewise, index function g forms a list index
(a pair of name sets) from a list index (two, curried name sets) and an element
index. By choosing type α, sort γ and index functions f and g, we can recover
integer lists, and lists of integer lists as special cases:
Integer lists:
α :≡ Int
γ :≡ 1
f :≡ λ(). λ(). ()
g :≡ λX. λY. λ(). (X, Y)

Lists of integer lists:
α :≡ List[−; −] Int
γ :≡ NmSet × NmSet
f :≡ λ(X1 , Y1 ). λ(X2 , Y2 ). (X1 ⊥ X2 , Y1 ⊥ Y2 )
g :≡ λX1 . λY1 . λ(X2 , Y2 ). (X1 ⊥ X2 , Y1 ⊥ Y2 )

On the left, we express list of integers by choosing α :≡ Int and γ :≡ 1,
the sort of Int’s (trivial) type index. On the right, we express lists of integer
lists by choosing α :≡ List[−; −] Int, the type of integer lists, and define f to
accumulate name sets for the inner lists, and g to accumulate name sets for both
the inner and outer lists. In this case, the resulting functions f and g happen to
be isomorphic.

35

B

Omitted Definitions, Figures, and Remarks

`·:Γ

emp

S`Γ

Γ `v:A

Γ (p) = A

` (S, p : v) : Γ

S`Γ

ref

Γ `e:E

Γ (p) = E

` (S, p : e) : Γ

thunk

Fig. 17. Store typing: S ` Γ , read “store S typed by Γ ”.

Pointers p, q ::= n
Stores
S ::= ·
| S, p:v
| S, p:e @ M

name constants
empty store
p points to value v
p points to thunk e, run in scope M

Notation: S{p7→v} and S{p7→e@M} extend S at p
when p ∈
/ dom(S)
S{p7→v} and S{p7→e@M} overwrite S at p when p ∈ dom(S)

S1 `M
m e ⇓ S2 ; t

Under store S in namespace M at current node m,
expression e produces new store S2 and result t

0
S1 `M
m [v2 /x2 ][v1 /x1 ]e ⇓ S2 ; e

S1 `M
m

split((v1 , v2 ), x1 .x2 .e) ⇓ S2 ; e

0

split

0
S1 `M
m e1 ⇓ S1 ; ret(v)
0
M
S1 `m [v/x]e2 ⇓ S20 ; e20
0
0
S10 `M
m let(e1 , x.e2 ) ⇓ S2 ; e2
1 ◦M2
S1 `M
e ⇓ S2 ; e 0
m
1
S1 `M
m

scope(M2 , e) ⇓ S2 ; e

(M n) ⇓M p
S1 `M
m

let

S

`M
m

thunk(name n, e) ⇓ S2 ; ret(thunk p)

force(thunk p) ⇓ S2 ; t

force

case(inji v, x1 .e1 , x2 .e2 ) ⇓ S2 ; e 0

0
S1 `M
m e1 ⇓ S1 ; λx. e2
M
S1 `m [v/x]e2 ⇓ S20 ; e20
0
0
S10 `M
m e1 v ⇓ S2 ; e2

M1 ⇓M λa. M2

scope

S1 {p7→e @ M} = S2

S(p) = e @ M0
0
S1 `M
e ⇓ S2 ; t
p
S1 `M
m

0

0
S1 `M
m [vi /xi ]ei ⇓ S2 ; e

S1 `M
m

[n/a]M2 ⇓M p

(M n) ⇓M p
S1 `M
m

S

name-app

S1 {p7→v} = S2

ref(name n, v)
⇓ S2 ; ret(ref p)

S(p) = v
`M
m

app

M1 (name n) ⇓ S; ret(name p)
thunk

get(ref p) ⇓ S; ret(v)

get

case

S `M
m t ⇓ S; t

ref

term

Fig. 18. Dynamic semantics, complete

In Figure 19, we write
D by Rulename (Dlist) reads R writes W
to mean that rule Rulename concludes D and has subderivations Dlist. For example, D by Eval-scope(D0 ) reads R writes W provided that D reads R writes W,
where D0 derives the only premise of Eval-scope.

36

D by Eval-term() reads ∅ writes ∅
D by Eval-app(D1 , D2 ) reads R1 ∪ R2 writes W1 ⊥ W2 if
D1 reads R1 writes W1
and D2 reads R2 writes W2
D by Eval-bind(D1 , D2 ) reads R1 ∪ R2 writes W1 ⊥ W2 if
D1 reads R1 writes W1
and D2 reads R2 writes W2
D by Eval-scope(D0 ) reads R writes W if
D by Eval-fix(D0 ) reads R writes W if
D by Eval-case(D0 ) reads R writes W if
D by Eval-split(D0 ) reads R writes W if

D0 reads R writes W

D0 reads R writes W
D0 reads R writes W
D0 reads R writes W

D by Eval-ref() reads ∅ writes p where e = ref(name n, v) and p ≡ M n
D by Eval-thunk() reads ∅ writes p where e = thunk(name n, e0 ) and p ≡ M n
D by Eval-get() reads p writes ∅ where e = get(ref p)
D by Eval-force() reads q, R 0 writes W 0 where e = force(thunk q)
and
D 0 reads R 0 writes W 0
where D 0 is the derivation that computed t
Fig. 19. Read- and write-sets of a non-incremental evaluation derivation

37

Γ `A:K

Under Γ , value type A has kind K
Γ ` A1 : type
Γ ` A2 : type
k-binop
(α : K) ∈ Γ
(d : K) ∈ Γ
Γ
`
(A
1 + A2 ) : type
k-typevar
k-tycon
Γ `α:K
Γ `d:K
Γ ` (A1 × A2 ) : type

Γ ` unit : type

k-unit

Γ ` i : NmSet
Γ ` Nm[i] : type

k-name

Γ ` i : NmSet

Γ ` A : type

Γ ` (Ref[i] A) : type

k-ref

Γ ` A : (type ⇒ K)
Γ ` A : (γ ⇒ K)
Γ ` B : type
Γ `i:γ
k-thk
k-app-type
k-app-index
Γ ` (Thk[i] E) : type
Γ ` (A B) : K
Γ ` A[i] : K
Γ ` i : NmSet
Γ ` E efftype

Γ ` C ctype

Under Γ , computation type C is well-formed

Γ ` A : type
Γ ` (F A) ctype

Γ `  wf-effects

Γ ` A : type

ctype-lift

Γ ` E efftype

Γ ` (A → E) ctype

Under Γ , effects  are well-formed
Γ ` W : NmSet

Γ ` R : NmSet

Γ ` hW; Ri wf-effects

Γ ` P prop

Under Γ , proposition P is well-formed
Γ ` P1 prop
Γ ` tt prop

Γ ` E efftype
Γ ` C ctype

ctype-arr

Γ `i:γ

Γ ` P2 prop

Γ ` (P1 and P2 ) prop

wf-eff

Γ `j:γ

Γ ` (i ⊥ j : γ) prop
Γ ` (i ≡ j : γ) prop

Under Γ , type-with-effects E is well-formed
Γ `  wf-effects

Γ ` (C  ) efftype

etype-eff

Γ, a : γ, P ` E efftype
Γ ` (∀a : γ | P. E) efftype

Γ, α : K ` E efftype
Γ ` (∀α : K. E) efftype
etype-idx

Fig. 20. Kinding and well-formedness for types and effects

etype-poly

38

B.1

Remarks

Why distinguish computation types from types-with-effects? Can we unify computation types C and types-with-effects E? Not easily. We have two computation
types, F and →. For F, the expression being typed could create a thunk, so we
must put that effect somewhere in the syntax. For →, applying a function is
(per call-by-push-value) just a “push”: the function carries no effects of its own
(though its codomain may need to have some). However, suppose we force a
thunked function of type A1 → (A2 → · · · ) and apply the function (the contents of the thunk) to one argument. In the absence of effects, the result would
be a computation of type A2 → · · · , meaning that the computation is waiting
for a second argument to be pushed. But, since forcing the thunk has the effect
of reading the thunk, we need to track this effect in the result type. So we cannot
return A2 → · · · , and must instead put effects around (A2 → · · · ). Thus, we
need to associate effects to both F and →, that is, to both computation types.
Now we are faced with a choice: we could (1) extend the syntax of each
connective with an effect (written next to the connective), or (2) introduce a
“wrapper” that encloses a computation type, either F or →. These seem more
or less equally complicated for the present system, but if we enriched the language with more connectives, choice (1) would make the new connectives more
complicated, while under choice (2), the complication would already be rolled
into the wrapper. We choose (2), and write the wrapper as C  , where C is a
computation type and  represents effects.
Where should these wrappers live? We could add C   to the grammar of
computation types C. But it seems useful to have a clear notion of the effect
associated with a type. When the effect on the outside of a type is the only
effect in the type, as in (A1 → F A2 )  , “the” effect has to be . Alas, types
like (C  1 )  2 raise awkward questions: does this type mean the computation
does 2 and then 1 , or 1 and then 2 ?
We obtain an unambiguous, singular outer effect by distinguishing typeswith-effects E from computation types C. The meta-variables for computation
types appear only in the production E ::= C  , making types-with-effects E the
“common case” in the grammar. Many of the typing rules follow this pattern,
achieving some isolation of effect tracking in the rules.

C

Omitted Lemmas and Proofs

Lemma 1 (Index-level weakening).
1. If Γ ` M : γ then Γ, Γ 0 ` M : γ.
2. If Γ ` i : γ then Γ, Γ 0 ` i : γ.
3. If Γ ` A : K then Γ, Γ 0 ` A : K.
Proof. By induction on the given derivation.
Lemma 2 (Weakening).

39

1. If Γ ` e : A then Γ, Γ 0 ` e : A.
2. If Γ `M e : C then Γ, Γ 0 `M e : C.
Proof. By induction on the given derivation, using Lemma 20 (Weakening of
semantic equivalence and apartness) (for example, in the case for the value typing
rule ‘name’) and Lemma 1 (Index-level weakening) (for example, in the case for
the computation typing rule ‘AllIndexElim’).
Lemma 3 (Substitution).

1. If Γ ` v : A and Γ, x : A ` e : C then Γ ` [v/x]e : C.

2. If Γ ` v : A and Γ, x : A ` v 0 : B then Γ ` [v/x]v 0 : B.
Proof. By mutual induction on the derivation typing e (in part 1) or v 0 (in part
2).
Lemma 4 (Canonical Forms). If Γ store-type and Γ ` v : A, then
1. If A = 1
then v = ().
2. If A = (B1 × B2 )
then v = (v1 , v2 ).
3. If A = (B1 + B2 )
then v = inji v
where i ∈ {1, 2}.
4. If A = (Nm[X])
then v = name n where Γ ` n ∈ X.
5. If A = (Ref[X] A0 )
then v = ref n
where Γ ` n ∈ X.
6. If A = (Thk[X] E)
then v = thunk n where Γ ` n ∈ X.
Nm
7. If A = (Nm →
Nm)[M] then v = nmfn Mv where M =β (λa. M 0 )
Nm
and · ` (λa. M 0 ) : (Nm →
Nm)
and Mv =β M.
Proof. In each part, exactly one value typing rule is applicable, so the result
follows by inversion.
Lemma 5 (Application and membership commute). If Γ ` n ∈ i and p =β M(n)
then Γ ` p ∈ M(i).
Proof. The set M(i) consists of all elements of i, but mapped by function M.
The name p is convertible to the name M(n). Since n ∈ i, we have that p is in
the M-mapping of i, which is M(i).
In each case, we write “Z” to the left of each goal, as we prove it.
Theorem 1 (Subject Reduction).
Nm
If Γ1 store-type and Γ1 ` M : Nm →
Nm and S derives Γ1 `M e : C  hW; Ri
and ` S1 : Γ1 and D derives S1 `M
e
⇓ S2 ; t then
m
there exists Γ2 ⊇ Γ1 such that Γ2 store-type and ` S2 : Γ2 and Γ2 ` t : C  h∅; ∅i
and D reads RD writes WD and hWD ; RD i  hW; Ri.
Proof. By induction on the typing derivation S.

40

– Case

Γ1 ` v : A

Γ1 `

M

 ret
ret(v) : (F A)  h∅; ∅i

(e = t) and (S1 = S2 )
Given
(RD = WD = R = W = ∅) 00
(Γ2 = Γ1 )
Suppose
Z
` S2 : Γ2
by above equalities
00
Z Γ2 ` t : C  h∅, ∅i
Z
D reads RD writes WD By Def. 2
Z
hWD ; RD i  hW; Ri
All are empty
– Case

Γ1 ` v : Ref[X] A

get
Γ1 ` get(v) : F A  h∅; Xi
M

(W = ∅) and (R = X) Given
Γ1 ` v : Ref[X] A
Given
∃p. (v = ref p)
Lemma 4 (Canonical Forms)
00
Γ1 ` p ∈ X
Γ1 (p) = A
By inversion of value typing
∃vp . S1 (p) = vp
Inversion on ` S1 : Γ1
00
Γ1 ` vp : A
(Γ2 = Γ1 ) and (t = ret(vp ))
Suppose
(RD = {p}) and (WD = ∅ = W) 00
Z
` S2 : Γ2
By above equalities
00
Z Γ2 ` t : C  h∅, ∅i
Z D reads RD writes WD By Def. 2
Z hWD ; RD i  hW; Ri
By above equality WD = W = ∅,
. . . and inequality for (RD = {p}) ⊆ (X = R).
– Case

Γ1 ` v : Thk[X] (C  )
Γ1 `

M

force(v) : C  (h∅; Xi then )

 force

Γ `e:τ
Given
Γ `e : τ
Given
(W = ∅) and (R = X) Given
Γ1 ` v : Thk[X] (C  ) Given
∃p. (v = thunk p)
Lemma 4 (Canonical Forms)
00
Γ1 ` p ∈ X
Γ1 (p) = (C  )
By inversion of value typing
∃ep . S1 (p) = ep
Inversion on ` S1 : Γ1
00
S0 :: Γ1 ` ep : (C  )

41

D0 :: S1 ` M
Inversion of D
m ep ⇓ S2 ; t
Z
` S2 : Γ2
By i.h. on S0 and D0
00
Z Γ2 ` t : C  h∅, ∅i
D0 reads RD writes WD 00
00
hWD0 ; RD0 i  hW; Ri
Z
D reads RD0 writes WD0 By Def. 2
Z
hWD0 ; RD0 i  hW; Ri
by above equality WD = W = ∅,
. . . and inequality (RD = {p}) ⊆ (X = R).
– Case

Nm
Γ1 ` v : (Nm →
Nm)[M 0 ]

0

Γ1 `M◦M e0 : C  hW; Ri

Γ1 `M scope(v, e0 ) : C  hW; Ri

scope

0

S0 :: Γ1 `M◦M e0 : C  hW; Ri
Subderivation 2 of S
D ::
S1 `M
scope(v,
e
)
⇓
S
;
t
Given
0
2
m
M◦M 0
D0 ::
S1 `m
e0 ⇓ S2 ; t
By inversion (scope)

Z
Z

Z
Z

Nm
Γ1 ` M : Nm →
Nm
Assumption
Nm
Γ1 ` v : (Nm → Nm)[M 0 ]
Subderivation 1 of S
Nm
0
Γ1 ` M : Nm → Nm
By inversion
Γ1 , x : Nm ` M 0 x : Nm
By rule t-app
Γ1 , x : Nm ` M (M 0 x) : Nm
By rule t-app
Nm
Γ1 ` λx. M (M 0 x) : Nm →
Nm By rule t-abs
Nm
0
Γ1 ` (M ◦ M ) : Nm → Nm
By definition of M ◦ M 0
` S2 : Γ2
By i.h. on S0
00
Γ2 ` t : C  h∅; ∅i
00
D0 reads RD0 writes WD0
00
hWD0 ; RD0 i  hW; Ri
D reads RD writes WD
By Def. 2
hWD ; RD i = hWD0 ; RD0 i 00
hWD ; RD i  hW; Ri
By above equalities

– Case

Γ1 ` v : Nm[X]
Γ1 `

M

Γ1 ` e : E

thunk(v1 , v2 ) : F (Thk[M(X)] E)  hM(X); ∅i

thunk

C = F (Thk[M(X)] E) and R = ∅ and W = M(X) Given from S
Γ1 ` v : Nm[X]
Subderivation
(v = name n) and (n ∈ X)
By Lemma 4
M n ⇓ p and RD = ∅ and WD = {p}
Given from D
00
S2 = (S1 , p : e)
Γ2 = (Γ1 , p : Thk[p] E) Suppose
Z ` S2 : Γ2
By rule (Fig. 17)
Γ2 (p) = E
By inversion of value typing

42

Γ2 ` ref p : Ref[p] E
By rule thunk
Z Γ2 `M ret(thunk p) : F (Thk[p] A)  h∅; ∅i By rule ret
Z D reads RD writes WD and WD = {p}
By Def. 2
n∈X
Above
M(n) ∈ M(X)
Name term application is pointwise
M(n) ∈ W
By above equality
M(n) = p
{p} ⊆ W
By set theory
Z hWD ; RD i  hW; Ri
– Case

Γ1 ` v1 : Nm[X]
Γ1 `

M

Γ1 ` v 2 : A

ref(v1 , v2 ) : F (Ref[M(X)] A)  hM(X); ∅i

ref

C = F (Ref[M(X)] A) and R = ∅ and W = M(X) Given from S
Γ1 ` v1 : Nm[X]
Subderivation
(v1 = name n) and (n ∈ X)
Lemma 4 (Canonical Forms)
M n ⇓ p and RD = ∅ and WD = {p} Given from D
00
S2 = (S1 , p : v2 )
Γ2 = (Γ1 , p : Ref[p] A)
Suppose
Z ` S2 : Γ2
By rule (Fig. 17)
Γ2 (p) = A
By inversion of value typing
Γ2 ` ref p : Ref[p] A
By rule ref
M
Z Γ2 ` ret(ref p) : ret(Ref[p] A)  h∅; ∅i By rule ret
Z D reads RD writes WD and WD = {p}
By Def. 2
n∈X
Above
M(n) ∈ M(X)
Name term application is pointwise
M(n) ∈ W
By above equality
M(n) = p
{p} ⊆ W
By set theory
Z hWD ; RD i  hW; Ri
– Case Γ `M e : (F A   )
1
1
1

Γ1 , x : A `M e2 : (C  2 )

Γ1 `M let(e1 , x.e2 ) : C  (1 then 2 )
` S1 : Γ1
S1 :: Γ1 `M e1 : F A  1
D1 :: S1 `M
m e1 ⇓ S12 ; t1
exists Γ12 ⊇ Γ1 such that S12 : Γ12
Γ12 ` t1 : F A  h∅; ∅i
D1 reads RD1 writes WD1
hWD1 ; RD1 i  1
hWD1 ; RD1 i  hW1 , R1 i

let

Given
Subderivation 1 of S
Subderivation 1 of D
By i.h. on S1
00
00
00
00

43

Γ12 ` v : A

S2 ::

D2 ::
Z
Z

inversion of typing rule ret,
for terminal computation t1
M
Γ1 , x : A ` e2 : C  2
Subderivation 2 of S
Γ12 , x : A `M e2 : C  2
Lemma 2 (Weakening)
Γ12 `M [v/x]e2 : C  2
Lemma 3 (Substitution)
S12 `M
[v/x]e
⇓
S
;
t
Subderivation
2 of D
2
2 2
m
exists Γ2 ⊇ Γ12 ⊇ Γ1 such that By i.h. on S2
00
` S2 : Γ2
M
00
Γ2 ` t2 : C  h∅; ∅i
00
D2 reads RD2 writes WD2
00
hWD2 ; RD2 i  2
00
hWD2 ; RD2 i  hW2 , R2 i

W1 ⊥ W2 and R1 ⊥ W2
WD1 ⊥ WD2 and RD1 ⊥ WD2
WD = WD1 ⊥ WD2
RD = RD1 ∪ (RD2 − WD1 )
Z D reads RD writes WD
Z hWD , RD i  hW, Ri
– Case Γ `M e : (A → E)   
1
Γ`

M

Definition of 1 then 2
WD1 ⊆ W1 ; WD2 ⊆ W2 ; RD1 ⊆ R1
By Def. 2
00
00

Since WD ⊆ W and RD ⊆ R
Γ `v:A

(e v) : (E after 1 )

app

Similar to the case for let.
– Case Γ `M v : (A × A )
1
2

Γ, x1 : A1 , x2 : A2 `M e : E

Γ `M split(v, x1 .x2 .e) : E

split

Similar to the case for let, using Lemma 4 (Canonical Forms).
– Case
M

Γ`

v : (A1 + A2 )

Γ, x1 : A1 `M e1 : E
Γ, x2 : A2 `M e2 : E

Γ `M case(v, x1 .e1 , x2 .e2 ) : E

case

Similar to the case for let, using Lemma 4 (Canonical Forms).
– Case

Nm
Γ1 ` vM : (Nm →
Nm)[M]
Γ1 ` v : Nm[i]
name-app
Γ1 ` (vM v) : F (Nm[M(i)])  h∅; ∅i

Nm
Γ1 ` vM : (Nm →
Nm)[M] Given
vM = nmfn Mv
Lemma 4 (Canonical Forms)
00
M =β (λa. M 0 )
Nm
0
· ` λa. M : (Nm → Nm) 00
00
Mv = β M

44

Γ1 ` v : Nm[i]
v = name n
Γ `n∈i

Given
Lemma 4 (Canonical Forms)
00

M ⇓M (λa. M 0 )
[n/a]M 0 ⇓M p
p =β [n/a]M 0
=β (λa. M 0 )(n)
=β M(n)

By inversion on D (name-app)
00

By a property of ⇓M
By a property of =β
By a property of =β

(Γ2 = Γ1 ), (S2 = S1 ) Suppose
` S2 : Γ2
By above equalities and S1 ` Γ1

Z

Γ1 ` n ∈ i
p =β M(n)
Γ1 ` p ∈ M(i)

Above
Above
By Lemma 5

Γ1 ` name p : Nm[M(i)])
By
Z Γ1 ` ret(name p) : F (Nm[M(i)])  h∅; ∅i By
Z
D by Eval-name-app reads ∅ writes ∅ By
Z
(RD = R = ∅), (WD = W = ∅)
By

– Case

Γ1 , a : γ, P `M t : E
Γ1 `M t : (∀a : γ | P. E)

AllIndexIntro

S0 ::Γ1 , a : γ, P `M t : E
D0 ::
S1 `M
m e ⇓ S2 ; t
∃Γ2 ⊆ Γ1
Z
` S2 : Γ2
D0 reads RD0 writes WD0
Γ2 ` t : E
hRD0 ; WD0 i  hR; Wi
M
Z
Γ2 ` t : (∀a : γ. E)
Z
D reads RD writes WD
Z
hRD ; WD i  hR; Wi

– Case
Γ1 `M e : (∀a : γ | P. E)
M

Γ1 `

rule name
rule ret
Def. 2
above equalities

Γ1 ` i : γ
extract(Γ1 )

e : [i/a]E

Subderivation
Subderivation
By i.h.
00
00
00
00

By typing rule
By Def. 2
By set theory

[i/a]P

AllIndexElim

45

Γ1 `M e : (∀a : γ. E)
Subderivation
S1 `M
e
⇓
S
;
t
Subderivation
2
m
∃Γ2 ⊆ Γ1
By i.h.
00
Z
` S2 : Γ2
00
D0 reads RD0 writes WD0
00
Γ2 ` t : (∀a : γ. E)
00
hRD0 ; WD0 i  hR; Wi
Γ1 ` i : γ
Subderivation
Γ2 ` i : γ
By weakening
Z Γ2 `M t : [i/a]E
By typing rule
Z
D reads RD writes WD By Def. 2
Z
hRD ; WD i  hR; Wi
By set theory

S0 ::
D0 ::

– Case

Γ, α : K `M t : E
Γ `M t : (∀α : K. E)

AllIntro

Similar to the AllIndexIntro case.
– Case Γ `M e : (∀α : K. E)
M

Γ`

Γ `A:K

e : [A/α]E

AllElim

Similar to the AllIndexElim case.

D
D.1

Bidirectional Typing
Syntax

As discussed below, bidirectional typing requires some annotations, so we assume
that values v and expressions e have been extended with annotations (v : A) and
(e : A). We also assume that we have explicit syntactic forms e[i] and e[A],
which avoid guessing quantifier instantiations.
D.2

Bidirectional Typing Rules

The typing rules in Figures 11 and 12 are declarative: they define what typings are valid, but not how to derive those typings. The rules’ use of names
and effects annotations means that standard unification-based techniques, like
Damas–Milner inference, are not clearly applicable. For example, it is not obvious when to apply chk-AllIntro.
Following the tradition of DML, we obtain an algorithmic version of our
typing rules by defining a bidirectional system (Pierce and Turner 2000): we split
judgments with a colon into judgments with an arrow. Thus, the computation
typing judgment · · · e : E becomes two judgments. The first is the checking
judgment Γ `M e ⇐ E, in which the type E is already known—it is an input to

46

Γ `v⇒A

Γ `v⇐A

Under Γ , value v synthesizes type A
(x : A) ∈ Γ
vsyn-var
Γ `x⇒A

vsyn-anno

Under Γ , value v checks against type A

Γ ` () ⇐ unit

vchk-unit

Γ `N∈X
Γ ` (name N) ⇐ Nm[X]

Γ ` v1 ⇐ A 1

vchk-name
Γ `N∈X

Γ ` v2 ⇐ A 2

Γ ` (v1 , v2 ) ⇐ (A1 × A2 )
Γ ` Mv ⇒ (Nm Nm
→ Nm)

Γ (N) = E

Γ ` (thunk N) ⇐ (Thk[X] E)
Γ ` v ⇐ A1
Γ ` inj1 v ⇐ A1 + A2

Mv =β M

Γ ` (nmfn Mv ) ⇐ (Nm → Nm)[M]
Γ (N) = A

vchk-thunk

vchk-inj1

vchk-pair

Nm

Γ ` (ref N) ⇐ Ref[X] A
Γ `N∈X

Γ `v⇐A
Γ ` (v : A) ⇒ A

vchk-namefn

vchk-ref

Γ ` v ⇒ A1

A1 = A2

Γ ` v ⇐ A2
Γ ` v ⇐ A2
Γ ` inj2 v ⇐ A1 + A2

vchk-conv

vchk-inj2

Fig. 21. Bidirectional value typing

the algorithm. The second is the synthesis judgment Γ `M e ⇒ E, in which E is
not known—it is an output—and the rules construct E by examining e (and Γ ).
In formulating the bidirectional versions of value and computation typing
(Figures 21 and 22), we mostly follow the “recipe” of Dunfield and Pfenning
(2004): introduction rules check, and elimination rules synthesize. More precisely, the principal judgment—the judgment, either a premise or conclusion,
that has the connective being introduced or eliminated—is checking (⇐) for
introduction rules, and synthesizing (⇒) for elimination rules. In many cases,
once the direction of that premise (or conclusion) is determined, the direction
of the other judgments follows by considering what information is known (as
input, or as the output type of the principal judgment, if that judgment is synthesizing). For example, if we commit to checking the conclusion of ‘chk-lam’,
we should check the premise because its type is a subexpression of the type in
the conclusion. (Checking is more powerful than synthesis: every expression that
synthesizes also checks, but not all expressions that check can synthesize.)
When a synthesis (elimination) premise attempts to type an expression that
is a checking (introduction) form, the programmer must write a type annotation
(e : E). Thus, following the recipe means that we have a straightforward annotation discipline: annotations are needed only on redexes. While we could reduce
the number of annotations by adding synthesis rules—for example, allowing the
unit value () to synthesize unit—this makes the system larger without changing

47
Under Γ , within namespace M,
computation e synthesizes type-with-effects E

Γ `M e ⇒ (A → E)  1
M
Γ ` e⇐E
Γ `v⇐A
Γ ` E after 1 ≡ E 0
syn-anno
syn-app
Γ `M (e : E) ⇒ E
Γ `M (e v) ⇒ E 0

Γ `M e ⇒ E

Γ ` v ⇒ Thk[X] (C  )
Γ ` h∅; Xi then  ≡  0
Γ`

force(v) ⇒ C  

M

Γ ` v ⇒ Ref[X] A

syn-force

0

Γ`

Γ ` vM ⇒ (Nm Nm
→ Nm)[M]

M

Γ ` v ⇒ Nm[i]

Γ `N (vM v) ⇒ F (Nm[M[i]])  h∅; ∅i
Γ `M e ⇒ (∀a : γ | P. E)
M

Γ`

Γ `i:γ

extract(Γ )

Γ `A:K

Γ `M e[A] ⇒ [A/α]E

Γ `M e ⇐ E
Γ`

M

M

E1 = E2

Γ `M split(v, x1 .x2 .e) ⇐ E

chk-split

Γ `M e ⇐ (C  2 )

Γ `M case(v, x1 .e1 , x2 .e2 ) ⇐ E

Γ `M (λx. e) ⇐ (A→E)  h∅; ∅i

chk-case

Γ `M e1 ⇒ (F A)  1
Γ, x : A `M e2 ⇐ (C  2 )
Γ ` 1 then 2 ≡ 

 chk-ret
ret(v) ⇐ (F A)  h∅; ∅i
Γ, x : A `M e ⇐ E

chk-eff-subsume

Γ ` v ⇒ (A1 + A2 )
Γ, x1 : A1 `M e1 ⇐ E
Γ, x2 : A2 `M e2 ⇐ E

Γ `v⇐A

Γ`

syn-AllIndexElim

syn-AllElim

Γ `M e ⇒ (C  1 )
Γ ` 1  2

chk-conv

e ⇐ E2

Γ ` v ⇒ (A1 × A2 )
Γ, x1 : A1 , x2 : A2 `M e ⇐ E

M

[i/a]P

Under Γ , within namespace M,
computation e checks against type-with-effects E

e ⇒ E1
Γ`

syn-name-app

e[i] ⇒ [i/a]E

Γ `M e ⇒ (∀α : K. E)

syn-get

get(v) ⇒ (F A)  h∅; Xi

 chk-lam

Γ `M let(e1 , x.e2 ) ⇐ C  

chk-let

Γ ` v ⇐ Nm[X]

Γ `M

Γ `M e ⇐ E
chk-thunk

thunk(v, e) ⇐ F (Thk[M[X]] E)  hM[X]; ∅i

Γ ` v1 ⇐ Nm[X]
Γ ` v2 ⇐ A
chk-ref

Γ `M ref(v1 , v2 ) ⇐ F (Ref[M[X]] A)  hM[X]; ∅i
Γ ` v ⇒ (Nm Nm
→ Nm)[N 0 ]

0

Γ `N◦N e ⇐ (C  hW; Ri)

Γ `N scope(v, e) ⇐ (C  hW; Ri)
Γ, a : γ, P `M t ⇐ E
M

Γ`

t ⇐ (∀a : γ | P. E)

chk-AllIndexIntro

chk-scope

Γ, α : K `M t ⇐ E
Γ `M t ⇐ (∀α : K. E)

Fig. 22. Bidirectional computation typing

chk-AllIntro

48

its essential properties; for a discussion of the implications of such extensions in
a different context, see Dunfield and Krishnaswami (2013).
Dually, when an expression synthesizes but we are trying to derive a checking
judgment, we use (1) ‘vchk-conv’ for value typing, or (2) ‘chk-conv’ or ‘chk-effsubsume’ for computation typing. The latter rule allows effect subsumption;
together, ‘chk-conv’ and ‘chk-eff-subsume’ encode a subsumption rule, common
in bidirectional systems with subtyping, such as Dunfield and Pfenning (2004).

E

Bidirectional Typing Proofs

Theorem 2 (Soundness of Bidirectional Value Typing).
1. If Γ ` v ⇒ A, then there exists a value v 0 such that Γ ` v 0 : A and |v| = v 0 .
2. If Γ ` v ⇐ A, then there exists a value v 0 such that Γ ` v 0 : A and |v| = v 0 .
Proof. By induction on the given derivation.
Part (1): Proceed by cases on the rule concluding Γ ` v ⇒ A.
Case (x : A) ∈ Γ
vsyn-var
Γ `x⇒A
(x : A) ∈ Γ
Γ `x : A
|x| = x
Z Γ ` v 0 : A and |v| = v 0
Case

Given
By rule var
By definition of |−|
where v 0 = x and v = x

Γ ` v1 ⇐ A
vsyn-anno
Γ ` (v1 : A) ⇒ A

∃ v10 such that Γ ` v10 : A and |v1 | = v10 By inductive hypothesis
|(v1 : A)| = |v1 | = v10
By definition of |−|
and |v1 | = v10
0
0
Z
Γ ` v : A and |v| = v where v 0 = v10 and v = (v1 : A)
Part (2): Proceed by cases on the rule concluding Γ ` v ⇐ A.
Case
Γ ` () ⇐ unit

vchk-unit

Γ ` () : unit
By rule unit
|()| = ()
By definition of |−|
Z Γ ` v 0 : () and |v| = v 0 where v 0 = () and v = ()
Case Γ ` v ⇐ A
Γ ` v2 ⇐ A2
1
1
vchk-pair
Γ ` (v1 , v2 ) ⇐ (A1 × A2 )

49

∃ v10 such that Γ ` v10 : A1 and |v1 | = v10
∃ v20 such that Γ ` v20 : A2 and |v2 | = v20
Γ ` (v10 , v20 ) : (A1 × A2 )
|(v1 , v2 )| = (|v1 |, |v2 |) = (v10 , v20 )
Z
Case

By inductive hypothesis
By inductive hypothesis
By rule pair
By definition of |−|
|v1 | = v10 and |v2 | = v20
Γ ` v 0 : (A1 × A2 ) and |v| = v 0 where v 0 = (v10 , v20 )
and v = (v1 , v2 )

Γ `n∈X
vchk-name
Γ ` (name n) ⇐ Nm[X]

Γ `n ∈ X
Γ ` (name n) : Nm[X]
|(name n)| = (name n)
Z
Γ ` v 0 : Nm[X] and |v| = v 0
Case

Nm
Γ ` Mv ⇒ (Nm →
Nm)

Given
By rule name
By definition of |−|
where v 0 = (name n)
and v = (name n)

M v =β M

Γ ` (nmfn Mv ) ⇐ (Nm → Nm)[M]
Nm

vchk-namefn

Nm
Nm) and |Mv | = Mv0 By i.h.
∃ Mv0 such that Γ ` Mv0 : (Nm →
Mv =β M Given
|Mv | =β M Type erasure does not affect convertibility
Mv0 =β M Since |Mv | = Mv0
Nm
Nm)[M]
Γ ` (nmfn Mv0 ) : (Nm →
|(nmfn Mv )| = (nmfn |Mv |) = (nmfn Mv0 )

By rule namefn
By definition of |−|
and |Mv | = Mv0
Nm
0
0
Γ ` v : (Nm → Nm)[M] and |v| = v where v 0 = (nmfn Mv0 )
and v = (nmfn Mv )

Z

Case Γ ` n ∈ X
Γ (n) = A
vchk-ref
Γ ` (ref n) ⇐ Ref[X] A
Γ `n ∈ X
Γ (n) = A
Γ ` (ref n) : Ref[X] A
|(ref n)| = ref n
Z
Γ ` v 0 : Ref[X] A and |v| = v 0
Case

Given
Given
By rule ref
By definition of |−|
where v 0 = (ref n)
and v = (ref n)

Γ `n∈X
Γ (n) = E
 vchk-thunk
Γ ` (thunk n) ⇐ Thk[X] E

50

Γ `n ∈ X
Γ (n) = E
Γ ` (thunk n) : Thk[X] E
|(thunk n)| = thunk n
Z
Γ ` v 0 : Thk[X] E and |v| = v 0

Given
Given
By rule thunk
By definition of |−|
where v 0 = (thunk n)
and v = (thunk n)

Case Γ ` v ⇒ A
A1 = A2
1
1
vchk-conv
Γ ` v1 ⇐ A 2
∃ v10 such that Γ ` v10 : A1 and |v1 | = v10
A1 = A2
Γ ` v10 : A2
Z
Γ ` v 0 : A2 and |v| = v 0

By inductive hypothesis
Given
By rule conv
where v 0 = v10 and v = v1

Theorem 3 (Completeness of Bidirectional Value Typing).
If Γ ` v : A then there exist values v 0 and v 00 such that
1. Γ ` v 0 ⇒ A and |v 0 | = v
2. Γ ` v 00 ⇐ A and |v 00 | = v
Proof. By induction on the derivation of Γ ` v : A.
Case
Γ ` () : unit

unit

Γ ` () ⇐ unit
By rule vchk-unit
|()| = ()
By definition of |−|
Z
Γ ` v 00 ⇐ () and |v 00 | = v where v 00 = () and v = ()
Γ ` (() : unit) ⇒ unit
By rule vsyn-anno
|(() : unit)| = ()
By definition of |−|
0
0
Z
Γ ` v ⇒ () and |v | = v where v 0 = (() : unit) and v = ()
Case (x : A) ∈ Γ
var
Γ `x:A
(x : A) ∈ Γ
Given
Γ `x ⇒ A
By rule vsyn-var
|x| = x
By definition of |−|
Z Γ ` v 0 ⇒ A and |v 0 | = v where v 0 = x and v = x
Γ `x ⇐ A
By rule vchk-conv
00
00
Z Γ ` v ⇐ A and |v | = v where v 00 = x and v = x
and |x| = x

51

Case Γ ` v : A
Γ ` v2 : A 2
1
1
pair
Γ ` (v1 , v2 ) : (A1 × A2 )
∃ v100 such that Γ ` v100 ⇐ A1 and |v100 | = v1
∃ v200 such that Γ ` v200 ⇐ A2 and |v200 | = v2
Γ ` (v100 , v200 ) ⇐ (A1 × A2 )
00
00
|(v1 , v2 )| = (|v100 |, |v200 |) = (v1 , v2 )

By
By
By
By

inductive hypothesis
inductive hypothesis
rule vchk-pair
definition of |−|; |v100 | = v1 ; |v200 | = v2

Z Γ ` v 00 ⇐ (A1 × A2 ) and |v 00 | = v
where v 00 = (v100 , v200 ) and v = (v1 , v2 )
00
00
Γ ` ((v1 , v2 ) : (A1 × A2 )) ⇒ (A1 × A2 ) By rule vsyn-anno
|(v100 , v200 ) : (A1 × A2 )| = |(v100 , v200 )| = (v1 , v2 ) By definition of |−|; |(v100 , v200 )| = (v1 , v2 )
Z Γ ` v 0 ⇒ (A1 × A2 ) and |v 0 | = v where v 0 = (v100 , v200 ) and v = (v1 , v2 )
Case

Γ `n∈X
name
Γ ` (name n) : Nm[X]

Γ `n ∈ X
Given
Γ ` (name n) ⇐ Nm[X]
By rule vchk-name
|(name n)| = (name n)
By definition of |−|
00
00
Z
Γ ` v ⇐ Nm[X] and |v | = v where v 00 = (name n) and v = (name n)
Γ ` (name n : Nm[X]) ⇒ Nm[X] By rule vsyn-anno
|(name n : Nm[X])| = |(name n)| = (name n)
By definition of |−|
Z Γ ` v 0 ⇒ Nm[X] and |v 0 | = v where v 0 = (name n : Nm[X]) and v = (name n)
Case

Nm
Γ ` Mv : (Nm →
Nm)

Mv = β M

Γ ` (nmfn Mv ) : (Nm → Nm)[M]
Nm

∃ Mv0 such that
Nm
Nm) and |Mv0 | = Mv
Γ ` Mv0 ⇒ (Nm →
M v =β M
|Mv0 | =β M
Mv0 =β M

namefn

By inductive hypothesis
Given
Since |Mv0 | = Mv
Type annotation does not affect convertibility

Nm
Γ ` (nmfn Mv0 ) ⇐ (Nm →
Nm)[M]
By rule vchk-namefn
0
|(nmfn Mv )| = (nmfn |Mv0 |) = (nmfn Mv ) By definition of |−|
and |Mv0 | = Mv
Nm
00
00
Z Γ ` v ⇐ (Nm → Nm)[M] and |v | = v
where v 00 = (nmfn Mv0 ) and v = (nmfn Mv )
Nm
Nm
Γ ` (nmfn Mv0 : (Nm →
Nm)[M]) ⇒ (Nm →
Nm)[M] By rule vsyn-anno
Nm
|(nmfn Mv0 : (Nm → Nm)[M])| = (nmfn Mv )
By definition of |−|

52
Nm
Nm
Z Γ ` v 0 ⇒ (Nm →
Nm)[M] and |v 0 | = v where v 0 = (nmfn Mv0 : (Nm →
Nm)[M])

Case Γ ` n ∈ X
Γ (n) = A
ref
Γ ` (ref n) : Ref[X] A
Γ `n ∈ X
Given
Γ (n) = A
Given
Γ ` (ref n) ⇐ Ref[X] A
By rule vchk-ref
|(ref n)| = (ref n)
By definition of |−|
Z Γ ` v 00 ⇐ Ref[X] A and |v 00 | = v
where v 00 = (ref n) and v = (ref n)
Γ ` ((ref n) : Ref[X] A) ⇒ Ref[X] A
By rule vsyn-anno
|(ref n : Ref[X] A)| = |(ref n)| = (ref n) By definition of |−|
Z Γ ` v 0 ⇒ Ref[X] A and |v 0 | = v
where v 0 = (ref n : Ref[X] A)
and v = (ref n)
Case

Γ `n∈X
Γ (n) = E
 thunk
Γ ` (thunk n) : Thk[X] E

Γ `n ∈ X
Γ (n) = E

Γ ` (thunk n) ⇐ Thk[X] E
|(thunk n)| = (thunk n)

Z Γ ` v 00 ⇐ Thk[X] E and |v 00 | = v

Given
Given
By rule vchk-thunk
By definition of |−|
where v 00 = (thunk n)
and v = (thunk n)


Γ ` (thunk n : Thk[X] E ) ⇒ Thk[X] E By rule vsyn-anno

|(thunk n : Thk[X] E )| = thunk n
By definition of |−|


Z Γ ` v 0 ⇒ Thk[X] E and |v 0 | = v where v 0 = (thunk n : Thk[X] E )
and v = (thunk n)

Theorem 4 (Soundness of Bidirectional Computation Typing).
1. If Γ `M e ⇒ E, then there exists a value e 0 such that Γ `M e 0 : E and |e| = e 0
2. If Γ `M e ⇐ E, then there exists a value e 0 such that Γ `M e 0 : E and |e| = e 0
Proof. By induction on the given derivation.
Part (1): Proceed by case analysis on the rule concluding Γ `M e ⇒ E.
Case Γ `M e ⇒ (A → E)   
Γ `v⇐A
1
1
Γ `M (e1 v) ⇒ (E after 1 )

vchk-app

53


Γ `M e10 : (A → E)  1 and |e1 | = e10
Γ ` v 0 : A and |v| = v 0
Γ `M (e10 v 0 ) : (E after 1 )
|(e1 v)| = (|e1 | |v|) = (e10 v 0 )
M 0
Z Γ ` e : (E after 1 ) and |e| = e 0
Case

Γ ` v ⇒ Thk[X] (C  )
M

Γ`

force(v) ⇒ C  (h∅; Xi then )

By inductive hypothesis
By Thm. 2
By rule app
By definition of |−|
where e 0 = (e10 v 0 ) and e = (e1 v)

 syn-force

Γ ` v 0 : Thk[X] (C  ) and |v| = v 0
By Thm. 2

M
0
Γ ` force(v ) : C  (h∅; Xi then )
By rule force
|force(v)| = force(|v|) = force(v 0 ) By definition of |−|
and |v| = v 0

Z Γ `M e 0 : C  (h∅; Xi then ) and |e| = e 0 where e 0 = force(v 0 ) and e = force(v)
Case
M

Γ`

Γ ` v ⇒ Ref[X] A

syn-get
get(v) ⇒ F A  h∅; Xi

Γ ` v 0 : Ref[X] A and |v| = v 0
By Thm. 2

Γ `M get(v 0 ) : F A  h∅; Xi
By rule get
|get(v)| = get(|v|) = get(v 0 ) By the definition of |−|
and |v| = v 0

M 0
0
Z Γ ` e : F A  h∅; Xi and |e| = e where e 0 = get(v 0 ) and e = get(v)
Case

Nm
Γ ` vM ⇒ (Nm →
Nm)[M]
Γ ` v ⇒ Nm[i]

Γ `N (vM v) ⇒ F (Nm[M(i)])  h∅; ∅i

syn-name-app

Nm
0
0
Γ ` vM
: (Nm →
Nm)[M] and |vM | = vM
0
0
Γ ` v : Nm[i] and |v| = v
0
Γ ` N (vM
v 0 ) : F (Nm[M(i)])  h∅; ∅i
0
|(vM v)| = (|vM | |v|) = (vM
v 0)
Z Γ `M e 0 : F (Nm[M(i)])  h∅; ∅i and |e| = e 0

Case Γ `M e ⇒ (∀a : γ. E)

Γ `i:γ

Γ `M e[i] ⇒ [i/a]E
Γ `M e 0 : (∀a : γ. E) and |e| = e 0
Γ `i : γ
Z e[i] = |e 0 |
Z Γ `M e 0 : [i/a]E

By Thm. 2
By Thm. 2
By rule name-app
0
By definition of |−|; |vM | = vM
; |v| = v 0
0
where e 0 = (vM
v 0 ) and e = (vM v)

syn-AllIndexElim

By inductive hypothesis
Given
By |e| = e 0
By rule AllIndexElim

54

Case Γ `M e ⇒ (∀α : K. E)
Γ`

M

Γ `A:K

e[A] ⇒ [A/α]E

syn-AllElim

Similar to the syn-AllIndexElim case.
Case
Γ `M e1 ⇐ E
Γ `M (e1 : E) ⇒ E

syn-anno

Γ `M e10 : E and |e1 | = e10 By inductive hypothesis
|e1 : E| = |e1 | = e10 By the definition of |−|
and |e1 | = e10
M 0
0
Z Γ ` e : E and |e| = e where e 0 = e10 and e = (e1 : E)
Part (2): Proceed by case analysis on the rule concluding Γ `M e ⇐ E.
Case Γ `M e ⇒ (C   )
 
1

M

Γ`

1

e ⇐ (C  2 )

2

chk-eff-subsume

Z Γ `M e 0 : (C  1 ) and |e| = e 0 By inductive hypothesis
1  2
Given
Z Γ `M e 0 : (C  2 )
By rule eff-subsume
Case Γ ` v ⇒ (A × A )
1
2
Γ, x1 : A1 , x2 : A2 `M e1 ⇐ E
Γ `M split(v, x1 .x2 .e1 ) ⇐ E

chk-split

Γ ` v 0 : (A1 × A2 ) and |v| = v 0 By Thm. 2
Γ, x1 : A1 , x2 : A2 `M e10 : E and |e1 | = e10
By inductive hypothesis
M
0
Γ ` split(v, x1 .x2 .e1 ) : E
By rule split
|split(v, x1 .x2 .e1 )| = split(|v|, x1 .x2 .|e1 |)
= split(v 0 , x1 .x2 .e10 ) By definition of |−|
and |v| = v 0 , |e1 | = e10
M 0
0
Z Γ ` e : E and |e| = e where e 0 = split(v 0 , x1 .x2 .e10 )
and e = split(v, x1 .x2 .e1 )
Case
Γ ` v ⇒ (A1 + A2 )

Γ, x1 : A1 `M e1 ⇐ E
Γ, x2 : A2 `M e2 ⇐ E

Γ `M case(v, x1 .e1 , x2 .e2 ) ⇐ E

chk-case

Γ ` v 0 : (A1 + A2 ) and |v| = v 0
Γ, x1 : A1 `M e10 : E and |e1 | = e10
Γ, x2 : A2 `M e20 : E and |e2 | = e20
Γ `M case(v 0 , x1 .e10 , x2 .e20 ) : E
|case(v, x1 .e1 , x2 .e2 )| = case(|v|, x1 .|e1 |, x2 .|e2 |)
= case(v 0 , x1 .e10 , x2 .e20 )

By Thm. 2
By inductive hypothesis
By inductive hypothesis
By rule case
By definition of |−|
Since |v| = v 0 , |e1 | = e10 , |e2 | = e20

55

Z Γ `M e 0 : E and |e| = e 0 where e 0 = case(v 0 , x1 .e10 , x2 .e20 )
and e = case(v, x1 .e1 , x2 .e2 )
Case

Γ `v⇐A

M

Γ`

 chk-ret
ret(v) ⇐ (F A)  h∅; ∅i

Γ ` v 0 : A and |v| = v 0

Γ `M ret(v 0 ) : (F A)  h∅; ∅i
|ret(v)| = ret(|v|) = ret(v 0 )

By Thm. 2
By rule ret
By definition of |−|
and |v| = v 0

Z Γ `M e 0 : (F A)  h∅; ∅i and |e| = e 0 where e 0 = ret(v 0 ) and e = ret(v)
Case Γ `M e ⇒ (F A)  
1
1
Γ `M

Γ, x : A `M e2 ⇐ (C  2 )

chk-let
let(e1 , x.e2 ) ⇐ C  (1 then 2 )

Γ ` M e10 : (F A)  1 and |e1 | = e10
By inductive hypothesis
Γ, x : A ` M e20 : (C  2 ) and |e2 | = e20
By inductive hypothesis

M
0
0
Γ ` let(e1 , x.e2 ) : C  (1 then 2 ) By rule let
|let(e1 , x.e2 )| = let(|e1 |, x.|e2 |)
By definition of |−|
= let(e10 , x.e20 )
Since |e1 | = e10 , |e2 | = e20

Z Γ `M e 0 : C  (1 then 2 ) and |e| = e 0 where e 0 = let(e10 , x.e20 ) and e = let(e1 , x.e2 )
Case

Γ, x : A `M e1 ⇐ E
M

Γ`

(λx. e1 ) ⇐ (A → E)  h∅; ∅i

 chk-lam

Γ, x : A `M e10 : E and |e1 | = e10
By inductive hypothesis

Γ `M (λx. e10 ) : (A → E)  h∅; ∅i
By rule lam
|(λx. e1 )| = (λx. |e1 |) = (λx. e10 ) By definition of |−|
and |e1 | = e10

M 0
0
Z Γ ` e : (A → E)  h∅; ∅i and |e| = e where e 0 = (λx. e10 ) and e = (λx. e1 )
Case

Γ ` v ⇐ Nm[X]

Γ `M e1 ⇐ E1

chk-thunk
Γ ` thunk(v, e1 ) ⇐ F (Thk[M(X)] E1 )  hM(X); ∅i

Let E = F (Thk[M(X)] E1 )  hM(X); ∅i Assumption
∃ v 0 such that Γ ` v 0 : Nm[X] and |v| = v 0
By Thm. 2
0
M 0
0
∃ e1 such that Γ ` e1 : E and |e1 | = e1
By inductive hypothesis
Γ `M thunk(v 0 , e10 ) : E
By rule thunk
|thunk(v, e1 )| = thunk(|v|, |e1 |) = thunk(v 0 , e10 ) By definition of |−|
and |v| = v 0 , |e1 | = e10
M

Z Γ `M e 0 : E and |e| = e 0 where e 0 = thunk(v 0 , e10 ) and e = thunk(v, e1 )

56

Case

Γ ` v1 ⇐ Nm[X]

M

Γ`

Γ ` v2 ⇐ A

chk-ref
ref(v1 , v2 ) ⇐ F (Ref[M(X)] A)  hM(X); ∅i

∃ v10 such that Γ ` v10 : Nm[X] and |v1 | = v10
By Thm. 2
∃ v20 such that Γ ` v20 : A and |v2 | = v20
By Thm. 2

Γ `M ref(v10 , v20 ) : F (Ref[M(X)] A)  hM(X); ∅i By rule ref
|ref(v1 , v2 )| = ref(|v1 |, |v2 |) = ref(v10 , v20 )
By definition of |−|

Z Γ ` M e 0 : F (Ref[M(X)] A)  hM(X); ∅i
and |e| = e 0
where e 0 = ref(v10 , v20 ) and e = ref(v1 , v2 )
Case

Nm
Γ ` v ⇒ (Nm →
Nm)[N 0 ]

0

Γ `N◦N e1 ⇐ C  hW; Ri

Γ `N scope(v, e1 ) ⇐ C  hW; Ri
Nm
Γ ` v 0 : Nm →
Nm and |N 0 | = v 0
By
0
N◦N
0
0
Γ `
e1 : C  hW; Ri and |e1 | = e1 By
Γ `N scope(v 0 , e10 ) : C  hW; Ri
By
|scope(v, e1 )| = scope(|v|, |e1 |) = scope(v 0 , e10 ) By

chk-scope

inductive hypothesis
inductive hypothesis
rule scope
definition of |−|; |v| = v 0 ; |e10 | = e1

Z Γ `M e 0 : C  hW; Ri and |e| = e 0 where e 0 = scope(v 0 , e10 ) and e = scope(v, e1 )
Case

Γ, a : γ `M t ⇐ E
Γ `M t ⇐ (∀a : γ. E)

chk-AllIndexIntro

Γ, a : γ `M t 0 : E and |t| = t 0
By inductive hypothesis
Γ `M t 0 : (∀a : γ. E)
By rule AllIndexIntro
Z
Γ `M e 0 : (∀a : γ. E) and |e| = e 0 where e 0 = t 0 and e = t
Case

Γ, a : γ `M t ⇐ E
Γ `M t ⇐ (∀α : K. E)

chk-AllIntro

∃ t 0 such that Γ, a : γ `M t 0 : E and |t| = t 0
By inductive hypothesis
M 0
Γ ` t : (∀α : K. E)
By rule AllIntro
Z
Γ `M e 0 : (∀α : K. E) and |e| = e 0 where e 0 = t 0 and e = t
Case Γ `M e ⇒ E
1
Γ`

M

E1 = E2

e ⇐ E2

chk-conv

Z ∃ e 0 such that Γ `M e 0 : E1 and |e| = e 0 By inductive hypothesis
E1 = E2
Given
M 0
Γ ` e : E2
Since E1 = E2

57

Theorem 5 (Completeness of Bidirectional Computation Typing).
If Γ `M e : E, then there exists computations e 0 , e 00 such that
1. Γ `M e 0 ⇒ E and |e 0 | = e
2. Γ `M e 00 ⇐ E and |e 00 | = e
Proof. By induction on the derivation of Γ `M e : E.
Case Γ `M e : (C   )
1
M

Γ`

1  2

e : (C  2 )

eff-subsume

Γ `M e 0 ⇒ (C  1 ) and e = |e 0 | By inductive hypothesis
1  2
Given
Γ `M e 0 ⇐ (C  2 )
By chk-eff-subsume
M
0
Γ ` (e : (C  2 )) ⇒ (C  2 ) By syn-anno
|(e 0 : (C  2 ))| = |e 0 | = e
By definition of |−|
Z
Γ `M e 0 ⇒ (C  2 ) and |e 0 | = e
Z
Γ `M e 00 ⇐ (C  2 ) and |e 00 | = e where e 00 = (e 0 : (C  2 ))
Case Γ ` v : (A × A )
1
2
Γ, x1 : A1 , x2 : A2 `M e1 : E
Γ `M split(v, x1 .x2 .e1 ) : E

split

Γ, x1 : A1 , x2 : A2 ` e10 ⇐ E and e1 = |e10 |
By inductive hypothesis
Γ ` v 0 ⇒ (A1 × A2 ) and v1 = |v10 | By Thm. 3
Γ `M split(v 0 , x1 .x2 .e10 ) ⇐ E
By chk-split
M
0
0
Γ ` (split(v , x1 .x2 .e1 ) : E) ⇒ E By syn-anno
|(split(v 0 , x1 .x2 .e10 ) : E)| = |split(v 0 , x1 .x2 .e10 )| By definition of |−|
|split(v 0 , x1 .x2 .e10 )| = split(|v 0 |, x1 .x2 .|e10 |) By definition of |−|
split(|v 0 |, x1 .x2 .|e10 |) = split(v, x1 .x2 .e1 )
Since |v 0 | = v, |e10 | = e1
Z Γ ` e 0 ⇒ E and |e 0 | = e where e 0 = split(v 0 , x1 .x2 .e10 )
and e = split(v, x1 .x2 .e1 )
Z Γ ` e 00 ⇐ E and |e 00 | = e where e 00 = (split(v 0 , x1 .x2 .e10 ) : E)
and e = split(v, x1 .x2 .e1 )
Case
Γ ` v : (A1 + A2 )

Γ, x1 : A1 `M e1 : E
Γ, x2 : A2 `M e2 : E

Γ `M case(v, x1 .e1 , x2 .e2 ) : E

case

Γ ` v 0 ⇒ (A1 + A2 ) and |v 0 | = v
By
M 00
00
Γ, x1 : A1 ` e1 ⇐ E and |e1 | = e1
By
Γ, x2 : A2 `M e200 ⇐ E and |e200 | = |e2 |
By
Γ ` M case(v 0 , x1 .e100 , x2 .e200 ) ⇐ E
By
Γ ` M (case(v 0 , x1 .e100 , x2 .e200 ) : E) ⇒ E By

Thm. 3
inductive hypothesis
inductive hypothesis
rule chk-case
rule chk-conv

58

|(case(v 0 , x1 .e100 , x2 .e200 ) : E)| = |case(v 0 , x1 .e100 , x2 .e200 )| By definition of |−|
|case(v 0 , x1 .e100 , x2 .e200 )| = case(|v 0 |, x1 .|e100 |, x2 .|e200 |) By definition of |−|
case(|v 0 |, x1 .|e100 |, x2 .|e200 |) = case(v, x1 .e1 , x2 .e2 )
Since |v 0 | = v, |e100 | = e1 , |e200 | = e2
Z Γ `M e 0 ⇒ E and |e 0 | = e where e 0 = (case(v 0 , x1 .e100 , x2 .e200 ) : E)
and e = case(v, x1 .e1 , x2 .e2 )
Z Γ `M e 00 ⇐ E and |e 00 | = e where e 00 = case(v 0 , x1 .e100 , x2 .e200 )
and e = case(v, x1 .e1 , x2 .e2 )
Case

Γ `v:A
M

Γ`

ret(v) : (F A)  h∅; ∅i

 ret


Let E = (F A)  h∅; ∅i
Assumption
∃ v 00 such that Γ ` v 00 ⇐ A and |v 00 | = v By Thm. 3
Γ `M ret(v 00 ) ⇐ E
By rule chk-ret
Γ `M (ret(v 00 ) : E) ⇒ E
By syn-anno
00
00
|(ret(v ) : E)| = |ret(v )|
By definition of |−|
|ret(v 00 )| = ret(|v 00 |) = ret(v) By definition of |−|
and |v 00 | = v
Z
Γ `M e 0 ⇒ E and |e 0 | = e where e 0 = (ret(v 00 ) : E) and e = ret(v)
Z
Γ `M e 00 ⇐ E and |e 00 | = e where e 00 = ret(v 00 ) and e = ret(v)
Case Γ `M e : (F A)  
1
1

Γ, x : A `M e2 : (C  2 )

let
Γ `M let(e1 , x.e2 ) : C  (1 then 2 )

Let E = C  (1 then 2 )
Assumption
Γ ` M e10 ⇒ (F A)  1 and |e10 | = e1 By inductive hypothesis
Γ, x : A ` M e200 ⇐ (C  2 ) and |e200 | = e2 By inductive hypothesis
Γ ` M let(e10 , x.e200 ) ⇐ E
By rule chk-let
Γ ` M (let(e10 , x.e200 ) : E) ⇒ E
By rule chk-conv
0
00
0
00
|(let(e1 , x.e2 ) : E)| = |let(e1 , x.e2 )|
By definition of |−|
|let(e10 , x.e200 )| = let(|e10 |, x.|e200 |) = let(e1 , x.e2 ) By definition of |−|
and |e10 | = e1 , |e200 | = e2

Z Γ `M e 0 ⇒ E and |e 0 | = e where e 0 = (let(e10 , x.e200 ) : E) and e = let(e1 , x.e2 )
Z Γ `M e 00 ⇐ E and |e 00 | = e where e 00 = let(e10 , x.e200 ) and e = let(e1 , x.e2 )

Case

Γ, x : A `M e1 : E1
Γ `M (λx. e1 ) : (A → E1 )  h∅; ∅i

 lam

59


Let E = (A → E1 )  h∅; ∅i
∃ e100 such that Γ, x : A `M e100 ⇐ E1 and |e100 | = e1
Γ `M (λx. e100 ) ⇐ E
Γ `M ((λx. e100 ) : E) ⇒ E
|(λx. e100 )| = (λx. |e100 |) = (λx. e1 )

Assumption
By inductive hypothesis
By rule chk-lam
By syn-anno
By definition of |−|
and |e100 | = e1

Z Γ `M e 0 ⇒ E and |e 0 | = e where e 0 = ((λx. e100 ) : E) and e = (λx. e1 )
Z Γ `M e 00 ⇐ E and |e 00 | = e where e 00 = (λx. e100 ) and e = (λx. e1 )
Case Γ `M e : (A → E)   
1
1
M

Γ`

Γ `v:A

(e1 v) : (E after 1 )

app


∃ e10 such that Γ `M e10 ⇒ (A → E)  1 and |e10 | = e1
∃ v 00 such that Γ ` v 00 ⇐ A and |v 00 | = v
Γ `M (e10 v 00 ) ⇒ (E after 1 )
Γ `M (e10 v 00 ) ⇐ (E after 1 )
0 00
|(e1 v )| = (|e10 | |v 00 |) = (e1 v)

By inductive hypothesis
By Thm. 3
By rule syn-app
By rule chk-conv
By the definition of |−|
and |e10 | = e1 , |v 00 | = v

Z Γ `M e 0 ⇒ E and |e 0 | = e where e 0 = (e10 v 00 ) and e = (e1 v)
Z Γ `M e 00 ⇐ E and |e 00 | = e where e 00 = (e10 v 00 ) and e = (e1 v)
Case

Γ `M e1 : E

thunk
thunk(v, e1 ) : F (Thk[M(X)] E)  hM(X); ∅i
Γ ` v : Nm[X]

Γ `M


Let E = F (Thk[M(X)] E)  hM(X); ∅i Assumption
∃ v 00 such that Γ ` v 00 ⇐ Nm[X] and |v 00 | = v
By Thm. 3
∃ e100 such that Γ `M e100 ⇐ E and |e100 | = e1
By inductive hypothesis
M
00
00
Γ ` thunk(v , e1 ) ⇐ E
By rule chk-thunk
Γ `M (thunk(v 00 , e100 ) : E) ⇒ E
By rule syn-anno
|(thunk(v 00 , e100 ) : E)| = |thunk(v 00 , e100 )|
By definition of |−|
|thunk(v 00 , e100 )| = thunk(|v 00 |, |e100 |) = thunk(v, e1 ) By definition of |−|
and |v 00 | = v, |e100 | = e1
Z Γ `M e 0 ⇒ E and |e 0 | = e where e 0 = (thunk(v 00 , e100 ) : E) and e = thunk(v, e1 )
Z Γ `M e 00 ⇐ E and |e 00 | = e where e 00 = thunk(v 00 , e100 ) and e = thunk(v, e1 )

Case

Γ ` v : Thk[X] (C  )
M

Γ`

force(v) : C  (h∅; Xi then )

 force

60


Let E = C  (h∅; Xi then )
Assumption
Γ ` v 0 ⇒ Thk[X] (C  ) and |v 0 | = v By Thm. 3
Γ `M force(v 0 ) ⇒ E
By rule syn-force
Γ `M force(v 0 ) ⇐ E
By chk-conv
|force(v 0 )| = force(|v 0 |) = force(v)
By definition of |−|
and |v 0 | = v
Z Γ `M e 0 ⇒ E and |e 0 | = e where e 0 = force(v 0 ) and e = force(v)
Z Γ `M e 00 ⇐ E and |e 00 | = e where e 00 = force(v 0 ) and e = force(v)
Case

Γ ` v1 : Nm[X]

M

Γ`

Γ ` v2 : A

ref
ref(v1 , v2 ) : F (Ref[M(X)] A)  hM(X); ∅i


Let E = F (Ref[M(X)] A)  hM(X); ∅i Assumption
Γ ` v100 ⇐ Nm[X] and |v100 | = v1
By Thm. 3
Γ ` v200 ⇐ A and |v200 | = v2
By Thm. 3
Γ ` M ref(v100 , v200 ) ⇐ E
By rule chk-ref
M
00
00
Γ ` (ref(v1 , v2 ) : E) ⇒ E
By rule syn-anno
|(ref(v100 , v200 ) : E)| = |ref(v100 , v200 )|
By definition of |−|
|ref(v100 , v200 )| = ref(|v100 |, |v200 |) = ref(v1 , v2 ) By definition of |−|
and |v100 | = v1 , |v200 | = v2
Z Γ `M e 0 ⇒ E and |e 0 | = e where e 0 = (ref(v100 , v200 ) : E) and e = ref(v1 , v2 )
Z Γ `M e 00 ⇐ E and |e 00 | = e where e 00 = ref(v100 , v200 ) and e = ref(v1 , v2 )
Case
M

Γ`

Γ ` v : Ref[X] A

get
get(v) : F A  h∅; Xi

Γ ` v 0 ⇒ Ref[X] A and |v 0 | = v By Thm. 3

Γ ` M get(v 0 ) ⇒ F A  h∅; Xi By rule syn-get

Γ ` M get(v 0 ) ⇐ F A  h∅; Xi By rule chk-conv
|get(v 0 )| = get(|v 0 |) = get(v)
By definition of |−|
and |v 0 | = v

Z Γ `M e 0 ⇒ F A  h∅; Xi and |e 0 | = e where e 0 = get(v 0 ) and e = get(v)

Z Γ `M e 00 ⇐ F A  h∅; Xi and |e 00 | = e where e 00 = get(v 0 ) and e = get(v)

Case

Nm
Γ ` vM : (Nm →
Nm)[M]
Γ ` v : Nm[i]

Γ `N (vM v) : F (Nm[M(i)])  h∅; ∅i

name-app

61

0
|(vM

Nm
0
0
Γ ` vM
⇒ (Nm →
Nm)[M] and |vM
| = vM
0
0
Γ ` v ⇒ Nm[i] and |v | = v
0
Γ ` N (vM
v 0 ) ⇒ F (Nm[M(i)])  h∅; ∅i
N 0
Γ ` (vM v 0 ) ⇐ F (Nm[M(i)])  h∅; ∅i
0
0
v )| = (|vM
| |v 0 |) = (vM v)

By Thm. 3
By Thm. 3
By rule syn-name-app
By rule chk-conv
By definition of |−|
0
and |vM
| = vM , |v 0 | = v

0
Z Γ `N e 0 ⇒ F (Nm[M(i)])  h∅; ∅i and |e 0 | = e where e 0 = (vM
v 0 ) and e = (vM v)
0
Z Γ `N e 00 ⇐ F (Nm[M(i)])  h∅; ∅i and |e 00 | = e where e 00 = (vM
v 0 ) and e = (vM v)

Case

Nm
Γ ` v : (Nm →
Nm)[N 0 ]

0

Γ `N◦N e1 : C  hW; Ri

Γ `N scope(v, e1 ) : C  hW; Ri

scope

Let E = C  hW; Ri
Assumption
Nm
∃v 00 such that , Γ ` v 00 ⇒ (Nm →
Nm)[N 0 ] and |v 00 | = v By Thm. 3
0
∃e10 such that , Γ `N◦N e10 ⇐ E and |e10 | = e1
By inductive hypothesis
Γ `N scope(v 00 , e10 ) ⇐ E
By rule chk-scope
Γ `N (scope(v 00 , e10 ) : E) ⇒ E
By rule syn-anno
|(scope(v

00

|(scope(v 00 , e10 ) : E)| = |(scope(v 00 , e10 )| By definition of |−|
= scope(|v 00 |, |e10 |) = scope(v, e1 )
By definition of |−|

, e10 )|

Z Γ `M e 0 ⇒ E and |e 0 | = e where e 0 = (scope(v 00 , e10 ) : E) and e = scope(v, e1 )
Z Γ `M e 00 ⇐ E and |e 00 | = e where e 00 = scope(v 00 , e10 ) and e = scope(v, e1 )

Case

Γ, a : γ `M t : E
Γ `M t : (∀a : γ. E)

AllIndexIntro

∃ t 00 such that Γ, a : γ ` M t 00 ⇐ E and |t 00 | = t
By inductive hypothesis
Γ `M t 00 ⇐ (∀a : γ. E)
By rule chk-AllIndexIntro
Γ `M (t 00 : (∀a : γ. E)) ⇒ (∀a : γ. E) By rule syn-anno
|(t 00 : (∀a : γ. E))| = |t 00 | = t
By definition of |−|
and |t 00 | = t
Z Γ `M e 0 ⇒ (∀a : γ. E) and |e 0 | = e where e 0 = (t 00 : (∀a : γ. E)) and e = t
Z Γ `M e 00 ⇐ (∀a : γ. E) and |e 00 | = e where e 00 = t 00 and e = t
Case Γ `M e : (∀a : γ. E)
M

Γ`

e : [i/a]E

Γ `i:γ

AllIndexElim

62

∃ e 0 such that Γ ` M e 0 ⇒ (∀a : γ. E) and |e 0 | = e By inductive hypothesis
Γ `i : γ
Given
M 0
Γ ` e ⇒ [i/a]E
By rule syn-AllIndexElim
Γ `M e 0 ⇐ [i/a]E
By rule chk-conv
Z
Γ `M e 0 [i] ⇒ [i/a]E and |e 0 [i]| = e
Z
Γ `M e 0 [i] ⇐ [i/a]E and |e 0 [i]| = e
Case

Γ, a : γ `M t : E
Γ `M t : (∀α : K. E)

AllIntro

Similar to the AllIndexIntro case.
Case Γ `M e : (∀α : K. E)
M

Γ`

Γ `A:K

e : [A/α]E

AllElim

Similar to the AllIndexElim case.

F

Name Term Language

We define a restricted name term language for computing larger names from
smaller names. This language consists of the following:
– Syntax for names, name terms and sorts.
– Name term sorting: A judgment that assigns sorts to name terms.
– Big-step evaluation for name terms: A judgment that assigns name term
values to name terms.
– Semantic definition of equivalent and disjoint name terms.
– Logical proof rules for equivalent and disjoint name terms: Two judgements
that should be sound with respect to the semantic definitions of equivalence
and disjointness.
F.1

Name term equivalence and apartness

For instance, the following two functions have the same sort, and are apart:
Nm
λa. (a, a)
: Nm →
Nm ∗ Nm
Nm
λb. (b, hhleaf, bii) : Nm →
Nm ∗ Nm
Nm
These functions have a common sort Nm →
Nm ∗ Nm, which says that they map
a single name (of sort Nm) to a pair of names (of sort Nm ∗ Nm). These functions
are apart, and this apartness ultimately follows from reasoning about binary
composition of names: any name n is distinct from the binary composition of
the name constant leaf with name n.

63

These two name functions also have the same sort, but are not apart:
Nm
λa. (a, hha, leafii) : Nm →
Nm ∗ Nm
Nm
λb. (a, hhleaf, bii) : Nm → Nm ∗ Nm

In particular, when b = a = leaf, they will produce the same pair, namely (leaf, hhleaf, leafii).
Notice that these two functions are obviously not equivalent either: Given
any name n such that n 6= leaf, these two functions will produce two distinct
names. This follows from another reasoning principle for name composition:
binary composition with leaf in the first function is in a distinct order from that
in the second function, precisely when n 6= leaf.
Finally, these two functions are equivalent: Given equivalent arguments, they
will always produce equivalent results:
Nm
Nm
Nm
λa. λb. a b : (Nm →
Nm) →
Nm →
Nm

Nm
Nm
Nm
λa1 . λb1 . λa2 . λb2 . a2 b2 a1 b1 : (Nm → Nm) → Nm → Nm

To see this equivalence more clearly, imagine reducing the inner β-reduxes by
substituting a1 and b1 for a2 and b2 , respectively. After this reduction, the two
functions are α-equivalent.
Below, we give a semantic definition of both equivalence and disjointness, in
terms of the sorting and operational definitions given above.
These definitions are clear, but not immediately practical: for function sorts,
they universally quantify over all possible arguments for the function’s argument. Since these arguments can include names, which consist of arbitrary finite
binary trees, as well as other functions, there is not an obvious finite set of arguments to test while still being sound with respect to these definitions. For a
practical implementation of Typed Adapton, we seek definitions of equivalence
and disjointness that admit decision procedures, and are sound (and, ideally,
complete) with respect to these semantic definitions. For this purpose, we give
decidable logical rules that induct over the syntax of the two terms.
F.2

Semantic equivalence and disjointness

Below, we define semantic equivalence and disjointness of (sorted) name terms.
We define these semantic properties inductively, based on the common sort of
the name terms. In this sense, these definitions can be viewed as instances of
logical relations.
We define contexts Γ that relate two variables, either asserting that they are
equivalent, or disjoint:
Substitutions
σ ::= · | σ, (a 7→ N)
Relational sorting contexts
Γ ::= ·
(Hypothetical variable equivalence) | Γ, (a ≡ b : γ)
(Hypothetical variable apartness)
| Γ, (a ⊥ b : γ)

64

(·).1 = ·
(Γ, a ≡ b : γ).1 = (Γ ).1, a : γ
(Γ, a ⊥ b : γ).1 = (Γ ).1, a : γ

(·).2 = ·
(Γ, a ≡ b : γ).2 = (Γ ).2, b : γ
(Γ, a ⊥ b : γ).2 = (Γ ).2, b : γ

Definition 3 (Closing substitutions).
We define closing substitution pairs related by equivalence and disjointness assumptions in a context Γ . These definitions use and are used by the definitions
below for equivalence and apartness of open terms.
σ1 ≡ σ2 : Γ means
 that (x ≡ y : γ) ∈ Γ implies σ1 (x) = N and σ2 (y) = M
and · N ≡ M : γ
– σ1 ⊥ σ2 : Γ means
 that (x ⊥ y : γ) ∈ Γ implies σ1 (x) = N and σ2 (y) = M
and · N ⊥ M : γ
– σ1 ∼ σ2 : Γ means that σ1 ≡ σ2 : Γ and σ1 ⊥ σ2 : Γ

–

Definition 4 (Semantic equivalence). We define Γ M1 ≡ M2 : γ as follows:
(Γ ).1 ` M1 : γ and (Γ ).2 ` M2 : γ and,
for all σ1 , σ2 such that σ1 ≡ σ2 : Γ and [σ1 ]M1 ⇓ V1 and [σ2 ]M2 ⇓ V2 , we
have the following about V1 and V2 :
Values V1 and V2 of sort γ are equivalent, written V1 ≡ V2 : γ
Always
When V1 = n1 and V2 = n2 and n1 = n2 (identical binary trees)
When V1 = (V11 , V12 ) and V1 = (V21 , V22 )
and V11 ≡ V21 : γ1 and V21 ≡ V22 : γ2
Nm
γ1 → γ2 When V1 = λa1 . M1 and V2 = λa2 . M2 ,
and for all name terms N1 ≡ N2 : γ1 ,
[N1 /a1 ]M1 ⇓ W1 and [N2 /a2 ]M2 ⇓ W2 implies W1 ≡ W2 : γ2
Sort (γ)
1
Nm
γ1 ∗ γ2

Definition 5 (Semantic apartness). We define Γ M1 ⊥ M2 : γ as follows:
(Γ ).1 ` M1 : γ and (Γ ).2 ` M2 : γ and,
for all σ1 , σ2 such that σ1 ∼ σ2 : Γ and [σ1 ]M1 ⇓ V1 and [σ2 ]M2 ⇓ V2 , we
have the following about V1 and V2 :
Values V1 and V2 of sort γ are apart, written V1 ⊥ V2 : γ
Always
When V1 = n1 and V2 = n2 and n1 6= n2 (distinct binary trees)
When V1 = (V11 , V12 ) and V1 = (V21 , V22 )
and V11 ⊥ V21 : γ1 and V21 ⊥ V22 : γ2
Nm
γ1 → γ2 When V1 = λa1 . M1 and V2 = λa2 . M2 ,
and for all name terms N1 ≡ N2 : γ1 ,
[N1 /a1 ]M1 ⇓ W1 and [N2 /a2 ]M2 ⇓ W2 implies W1 ⊥ W2 : γ2
Sort (γ)
1
Nm
γ1 ∗ γ2

F.3

Metatheory of name term language

Some lemmas in this section are missing complete proofs and should be considered conjectures (Lemma 6 (Projections of syntactic equivalence)—Lemma 14
(Reflexivity of name term evaluation)).

65

Γ `M≡N:γ

The name terms M and N are equivalent at sort γ

(M ≡ N : γ) ∈ Γ
Γ `M≡N:γ

(Γ ).1 ` M : γ
(Γ ).2 ` M : γ

Eq-Var

Γ `M≡M:γ

Γ ` M1 ≡ M2 : γ
Γ ` M2 ≡ M3 : γ
Γ ` M1 ≡ M3 : γ
Γ ` M1 ≡ N1 : γ1

E-Refl

Γ ` M2 ≡ N2 : γ2

Γ ` M1 ≡ N1 : Nm

Eq-Lam

Γ ` M2 ≡ M20 : γ1

E-Sym

Eq-Pair

Γ ` M2 ≡ N2 : Nm

Γ ` hhM1 , M2 ii ≡ hhN1 , N2 ii : Nm

Γ ` λa. M ≡ λb. N : γ1 Nm
→ γ2

Γ `M≡N:γ

Eq-Trans

Γ ` (M1 , M2 ) ≡ (N1 , N2 ) : γ1 ∗ γ2


Γ, a ≡ b : γ1 ` M ≡ N : γ2

Γ `N≡M:γ

Eq-Bin

Γ ` M1 ≡ N1 : γ1 Nm
→ γ2
Γ ` M2 ≡ N2 : γ1
Γ ` M1 (M2 ) ≡ N1 (N2 ) : γ2

Γ, a ≡ a : γ1 ` M1 ≡ M10 : γ2

Γ ` (λa. M1 )M2 ≡ [M20 /a]M10 : γ2

Eq-App

Eq-β

Fig. 23. Deductive rules for showing that two name terms are equivalent

Lemma 6 (Projections of syntactic equivalence).
If Γ ` M1 ≡ M2 : γ, then Γ.1 ` M1 : γ and Γ.2 ` M2 : γ.
Lemma 7 (Compatibility of substitution with name term structure).
1. We have [σ](M1 , M2 ) = ([σ]M1 , [σ]M2 ).
2. We have [σ]hhM1 , M2ii = hh[σ]M1 , [σ]M2ii.
3. We have [σ](MN) = ([σ]M)([σ]N).
Lemma 8 (Determinism of evaluation up to substitution).
If Γ.1 ` M : γ, Γ.2 ` M : γ, σ1 ≡ σ2 : Γ , [σ1 ]M ⇓ V1 , and [σ2 ]M ⇓ V2 , then
there exists a V such that V1 = [σ1 ]V and V2 = [σ2 ]V.
Lemma 9 (Reflexivity of semantic equivalence).
1. If ` M : γ, then M ≡ M : γ.
2. If Γ.1 ` V : γ, Γ.2 ` V : γ, σ1 ≡ σ2 : Γ , V1 = [σ1 ]V, and V2 = [σ2 ]V, then
V1 ≡ V2 : γ.
Lemma 10 (Type safety).
If Γ ` M : γ, [σ]M ⇓ [σ]V, then Γ ` V : γ.
Lemma 11 (Symmetry of semantic equivalence).
1. If

σ1 ≡ σ2 : Γ , then

σ2 ≡ σ1 : Γ T .

66

Γ `M⊥N:γ

The name terms M and N are apart at sort γ

(a ⊥ b : γ) ∈ Γ
Γ `a⊥b:γ

Γ `N⊥M:γ

Var

Γ `M⊥N:γ

Γ ` M1 ≡ M2 : γ

Γ ` M2 ⊥ M3 : γ

Γ ` M1 ⊥ M3 : γ
Γ ` M1 ⊥ N1 : γ1
Γ ` (M1 , M2 ) ⊥ (N1 , N2 ) : γ1 ∗ γ2
Γ ` M2 ⊥ N2 : γ2
Γ ` (M1 , M2 ) ⊥ (N1 , N2 ) : γ1 ∗ γ2
Γ ` M1 ⊥ N1 : Nm
Γ ` hhM1 , M2 ii ⊥ hhN1 , N2 ii : Nm
Γ ` M2 ⊥ N2 : Nm
Γ ` hhM1 , M2 ii ⊥ hhN1 , N2 ii : Nm
Γ ` N1 ≡ N2 : Nm
Γ ` hhM, N1 ii ⊥ N2 : Nm

D-Proj1

D-Proj2

D-Bin1

Γ ` hhM2 , Nii ⊥ M1 : Nm

Γ, a ≡ b : γ1 ` M ⊥ N : γ2

D-EqTag2

D-EqTag1

Γ ` λa. M ⊥ λb. N : γ1 Nm
→ γ2
Γ ` M2 ≡ N2 : γ1

Γ ` M1 (M2 ) ⊥ N1 (N2 ) : γ2
Γ.1 ` M2 : γ2

D-trans

Γ ` M1 ≡ M2 : Nm

D-Bin2

Γ ` M1 ⊥ N1 : γ1 Nm
→ γ2

D-Sym

Γ.1, a : γ2 ` M1 : γ

D-App

Γ ` [M2 /a]M1 ⊥ N : γ

Γ ` (λa. M1 ) M2 ⊥ N : γ

D-Lam

D-β

Fig. 24. Deductive rules for showing that two name terms are apart

67

2. If V1 ≡ V2 : γ, then V2 ≡ V1 : γ.
3. If · M1 ≡ M2 : γ, then · M2 ≡ M1 : γ.
4. If Γ M1 ≡ M2 : γ, then Γ T M2 ≡ M1 : γ.
Lemma 12 (Evaluation respects semantic equivalence).
If Γ
M ≡ N : γ, σ1 ≡ σ2 : Γ , and [σ1 ]M ⇓ V1 , then there exists V2 such
that [σ2 ]N ⇓ V2 and V1 ≡ V2 : γ.
Lemma 13 (Closing substitutions respect syntactic equivalence).
If σ1 ≡ σ2 : Γ and Γ ` M1 ≡ M2 : γ, then · [σ1 ]M1 ≡ [σ2 ]M2 : γ.
Lemma 14 (Reflexivity of name term evaluation).
If Γ.1 ` M : γ, Γ.2 ` M : γ, σ1 ≡ σ2 : Γ , [σ1 ]M ⇓ V1 , and [σ2 ]M ⇓ V2 , then
V1 ≡ V2 : γ.
Lemma 15 (Transitivity of value equivalence).
If ` V1 : γ, ` V2 : γ, V1 ≡ V2 : γ, and V2 ≡ V3 : γ, then

V1 ≡ V3 : γ.

Proof. Uses strong normalization.
Conjecture 16 (Soundness of deductive equivalence). If Γ ` M1 ≡ M2 : γ then
Γ M1 ≡ M2 : γ.
Proof. By induction on the given derivation.
Case (a ≡ b : γ) ∈ Γ
Eq-Var
Γ `a≡b:γ
By definition of closing substitutions.
Case

(Γ ).1 ` M : γ
(Γ ).2 ` M : γ
Eq-Refl
Γ `M≡M:γ

By Lemma 8 (Determinism of evaluation up to substitution), Lemma 10
(Type safety), and Lemma 9 (Reflexivity of semantic equivalence).
Case Γ ` N ≡ M : γ
Eq-Sym
Γ `M≡N:γ
By Lemma 11 (Symmetry of semantic equivalence).
Case Γ ` M ≡ M : γ
1
2
Γ ` M2 ≡ M3 : γ
Eq-Trans
Γ ` M1 ≡ M3 : γ
By idempotency of flipping relational contexts, Lemma 12 (Evaluation respects semantic equivalence), inductive hypotheses on the two given subderivations, Lemma 11 (Symmetry of semantic equivalence), and Lemma 15 (Transitivity of value equivalence).

68

Case Γ ` M ≡ N : γ
Γ ` M2 ≡ N2 : γ2
1
1
1
Eq-Pair
Γ ` (M1 , M2 ) ≡ (N1 , N2 ) : γ1 ∗ γ2
By Lemma 7 (Compatibility of substitution with name term structure) and
inductive hypothesis.
Case Γ ` M ≡ N : Nm
Γ ` M2 ≡ N2 : Nm
1
1
Eq-Bin
Γ ` hhM1 , M2ii ≡ hhN1 , N2ii : Nm
By Lemma 7 (Compatibility of substitution with name term structure) and
inductive hypothesis.
Case Γ, a ≡ b : γ  ` M ≡ N : γ
1
2
Nm
Γ ` λa. M ≡ λb. N : γ1 →
γ2

Eq-Lam

By Barendregt’s Substitution Lemma and inductive hypothesis.
Case

Nm
Γ ` M 1 ≡ N1 : γ 1 →
γ2
Γ ` M 2 ≡ N2 : γ 1
Eq-App
Γ ` M1 (M2 ) ≡ N1 (N2 ) : γ2

By Lemma 7 (Compatibility of substitution with name term structure) and
inversion (teval-app) of resulting derivations, the inductive hypothesis on the
two given syntactic equivalence subderivations (of Eq-App), and definition of
semantic equivalence of arrow-sorted values, we get the result.
Case Γ ` M ≡ M 0 : γ
Γ, a ≡ a : γ1 ` M1 ≡ M10 : γ2
2
1
2
Eq-β
Γ ` (λa. M1 )M2 ≡ [M20 /a]M10 : γ2
Fix σ1 ≡ σ2 : Γ . Suppose [σ1 ]((λa. M1 )M2 ) ⇓ V1 and [σ2 ]([M20 /a]M10 ) ⇓
V2 . We need to show
V1 ≡ V2 : γ2 . By Lemma 7 (Compatibility of substitution with name term structure) and inversion of teval-app, [σ1 ]M2 ⇓ V
and [V/a]([σ1 ]M1 ) ⇓ V1 for some V. Hence, because Γ, a ≡ a : γ1 , we have
[σ1 , a 7→ V]M1 ⇓ V1 . Rewrite [σ2 ]([M20 /a]M10 ) ⇓ V2 as [σ2 , a 7→ [σ2 ]M20 ]M10 ⇓
V2 . By Lemma 13 (Closing substitutions respect syntactic equivalence), · ` V ≡
[σ2 ]M20 : γ1 . Therefore,
σ1 , a 7→ V ≡ σ2 , a 7→ [σ2 ]M20 : Γ, a ≡ a : γ1
By the inductive hypothesis on Γ, a ≡ a : γ1 ` M1 ≡ M10 : γ2 , we get
V2 : γ2 .

V1 ≡

Conjecture 17 (Soundness of deductive disjointness). If Γ ` M1 ⊥ M2 : γ then
Γ M1 ⊥ M2 : γ.
Conjecture 18 (Completeness of deductive equivalence). If Γ
then Γ ` M1 ≡ M2 : γ.

M1 ≡ M 2 : γ

Conjecture 19 (Completeness of deductive disjointness). If Γ
then Γ ` M1 ⊥ M2 : γ.

M1 ⊥ M2 : γ

69

G

Index term language

extract-assns(·) = ·
extract-assns(Γ, P) = extract-assns(Γ ), P
extract-assns(Γ, tt) = extract-assns(Γ )
extract-assns(Γ, (P1 and · · · and Pn )) = extract-assns(Γ ), P1 , . . . , Pn
for n ≥ 1, where each Pk
has the form i ⊥ j : γ or i ≡ j : γ
extract-assns(Γ, Z) = extract-assns(Γ ) where Z is not a proposition
extract-ctx(·) = ·
extract-ctx(Γ, a : γ) = extract-ctx(Γ ), (a ≡ a : γ)
extract-ctx(Γ, α : type) = extract-ctx(Γ )
extract-ctx(Γ, d : K) = extract-ctx(Γ )
extract-ctx(Γ, p : · · ·) = extract-ctx(Γ )
extract-ctx(Γ, x : A) = extract-ctx(Γ )
extract-ctx(Γ, P) = extract-ctx(Γ )
extract(Γ ) = (extract-assns(Γ ); extract-ctx(Γ ))
Fig. 25. Extraction function on typing contexts

G.1

Semantic equivalence and apartness of index terms

Definition 6 (Closing substitutions for index terms).
We define closing substitution pairs related by equivalence and disjointness assumptions in a context Γ . These definitions use and are used by the definitions
below for equivalence and apartness of open terms.
σ1 ≡ σ2 : Γ means
that (x ≡ y : γ) ∈ Γ implies σ1 (x) = i and σ2 (y) = j

and · i ≡ j : γ
–
σ1 ⊥ σ2 : Γ means
that (x ⊥ y : γ) ∈ Γ implies σ1 (x) = i and σ2 (y) = j

and · i ⊥ j : γ

– σ1 ∼ σ2 : Γ means that
σ1 ≡ σ2 : Γ and σ1 ⊥ σ2 : Γ
–

Definition 7 (Semantic equivalence of index terms). We define Γ i1 ≡ i2 : γ as
follows:
(Γ ).1 ` i1 : γ and (Γ ).2 ` i2 : γ and,
for all σ1 , σ2 such that σ1 ≡ σ2 : Γ and [σ1 ]i1 ⇓ j1 and [σ2 ]i2 ⇓ j2 , we have
the following about j1 and j2 :

70

i val

Index i is a value (it evaluates to itself)

{N} val

val-singleton

i⇓j

i val

j val

i ⊥ j val

i val

val-disj

j val

(i, j) val

val-pair

λa. i val

val-abs

Index i evaluates to index j

i val
i⇓i

i 1 ⇓ j1

value

i 2 ⇓ j2

i ⇓ i0
j ⇓ j0

i 0 ⊥ j 0 : NmSet

(i ⊥ j) ⇓ (i 0 ⊥ j 0 )

i ⇓ (j1 , j2 )

pair

(i1 , i2 ) ⇓ (j1 , j2 )

prjb i ⇓ jb

(i ∪ j) ⇓ (i 0 ∪ j 0 )
j ⇓ j0

union

[j 0 /a]i 0 ⇓ k

i(j) ⇓ k

j ⇓ j0

M[j 0 ] ; j 00
M[j] ⇓ j 00

M[X] ; Y

proj

i ⇓ λa. i 0

disj

i ⇓ i0
j ⇓ j0

app

map-set

Name term function M, applied to each member of X, yields name set Y

M(N) ⇓M V
M[{N}] ; {V}

M[X1 ] ; Y1

Single

M[X2 ] ; Y2

M[X1 ⊥ X2 ] ; Y1 ⊥ Y2

Apart

Fig. 26. Evaluation rules for indices

Γ `M∈X

Name term M is a member of name set X, assuming X val

Γ `M∈X
Γ ` M ∈ (X ⊥ Y)
Γ `M∈X
Γ ` M ∈ (X ∪ Y)

Γ `M∈Y

Apart1

Γ ` M ∈ (X ⊥ Y)
Γ `M∈Y

Union1

Γ ` M ∈ (X ∪ Y)

Γ ` M ≡ N : Nm
Γ ` M ∈ {N}
extract-assns(Γ ) ` X ≡ Y : NmSet

Union2

Single
Γ `N∈Y

Γ `N∈X

Γ `M∈
/X

Apart2

EqualNameSet

The name of name term M is not a member of name set X, assuming X val

Γ `M∈
/X

Γ `M∈
/Y

Γ `M∈
/ (X ⊥ Y)

Γ ` M ⊥ N : Nm

Apart

Γ `M∈
/∅

Γ `M∈
/ {N}
Empty

Fig. 27. Name term membership

Single

71

Sort γ
1
NmSet
γ1 ∗ γ2

Indices j1 and j2 of sort γ are equivalent, written
Always

When
M ∈ j1 if and only if
M ∈ j2
When j1 = (j11 , j12 ) and j1 = (j21 , j22 )
and j11 ≡ j21 : γ1
and j12 ≡ j22 : γ2
idx
γ1 →
γ2 When j1 = λa1 . X1 and j2 = λa2 . X2 ,
and for all name terms Y1 ≡ Y2 : γ1 ,
(λa1 . X1 )(Y1 ) ⇓ Z1 and (λa2 . X2 )(Y2 ) ⇓ Z2
implies
Z1 ≡ Z2 : γ2

j1 ≡ j2 : γ

Definition 8 (Semantic apartness of index terms). We define Γ
i1 ⊥ i2 : γ as
follows:
(Γ ).1 ` i1 : γ and (Γ ).2 ` i2 : γ and,
for all σ1 , σ2 such that σ1 ∼ σ2 : Γ and [σ1 ]i1 ⇓ j1 and [σ2 ]i2 ⇓ j2 , we have
the following about j1 and j2 :
Sort (γ) Index values j1 and j2 of sort γ are apart, written
1
Always

NmSet When
M ∈ j1 implies
M∈
/ j2

and
M ∈ j2 implies
M∈
/ j1
γ1 ∗ γ2 When j1 = (j11 , j12 ) and j1 = (j21 , j22 )
and j11 ⊥ j21 : γ1 and j12 ⊥ j22 : γ2
idx
γ1 →
γ2 When j1 = λa1 . X1 and V2 = λa2 . X2 ,
and for all name terms Y1 ≡ Y2 : γ1 ,
(λa1 . X1 )(Y1 ) ⇓ Z1 and (λa2 . X2 )(Y2 ) ⇓ Z2
implies Z1 ⊥ Z2 : γ2

j1 ⊥ j2 : γ

The next two definitions bridge the gap with the type system, in which
contexts ΓT also include propositions P. It is defined assuming that extract(ΓT )
(defined in Figure 25) has given us some propositions P1 , . . . , Pn and a relational
context Γ .
Definition 9 (Extended semantic equivalence of index terms).
We define P1 , . . . , Pn ; Γ i ≡ j : γ to hold if and only if
J (P1 ) and · · · and J (Pn ) implies Γ
where J (i Θ j : γ) = (Γ

i≡j:γ

i Θ j : γ).

Definition 10 (Extended semantic apartness of index terms).
We define P1 , . . . , Pn ; Γ i ⊥ j : γ to hold if and only if
J (P1 ) and · · · and J (Pn ) implies Γ
where J (i Θ j : γ) = (Γ

i⊥j:γ

i Θ j : γ).

When a typing context is weakened, semantic equivalence and apartness under the extracted context continue to hold:

72

Lemma 20 (Weakening of semantic equivalence and apartness).
If extract(ΓT ) i1 ≡ i2 : γ (respectively i1 ⊥ i2 : γ) then extract(ΓT , ΓT0 )
i2 : γ (respectively i1 ⊥ i2 : γ.

i1 ≡

Proof. By induction on ΓT0 .
We prove the ≡ part; the ⊥ part is similar.
– If ΓT0 = ·, we already have the result.
– If ΓT0 = (Γ 0 , P) then:
By i.h., extract(ΓT , Γ 0 ) i1 ≡ i2 : γ.
That is, extract-assns(ΓT , Γ 0 ); extract-ctx(ΓT , Γ 0 ) i1 ≡ i2 : γ.
By its definition, extract-ctx(ΓT , Γ 0 , P) = extract-ctx(ΓT , Γ 0 , P).
Therefore, we have extract-assns(ΓT , Γ 0 ); extract-ctx(ΓT , Γ 0 , P) i1 ≡ i2 : γ.
Adding an assumption before the semicolon only supplements the antecedent
in Def. 9, so
extract-assns(ΓT , Γ 0 , P); extract-ctx(ΓT , Γ 0 , P)

i1 ≡ i2 : γ

which was to be shown.
– If ΓT0 = (Γ 0 , a : γ) then by i.h.,
extract(ΓT , Γ 0 )

i1 ≡ i2 : γ

By definition of extract-ctx,
extract-ctx(ΓT , Γ 0 , a : γ) = extract-ctx(ΓT , Γ 0 ), a ≡ a : γ
By the i.h. and Def. 7, (extract-ctx(ΓT , Γ 0 )).1 ` i1 : γ We need to show that
(extract-ctx(ΓT , Γ 0 , a : γ)).1 ` i1 : γ, which follows by weakening on sorting.
The “.2” part is similar.
Since a does not occur in i1 and i2 , applying longer substitutions that include
a to i1 and i2 does not change them; thus, we get the same j1 and j2 as for
ΓT , Γ 0 .
– In the remaining cases of Z for ΓT0 = (Γ 0 , Z), neither extract-assns nor
extract-ctx change, and the i.h. immediately gives the result.

73

G.2

Deductive equivalence and apartness for index terms

Γ `i≡j:γ

The name terms i and j are equivalent at sort γ

(i ≡ j : γ) ∈ Γ
Γ `i≡j:γ

(Γ ).1 ` i : γ

Eq-Var

Γ `j≡i:γ
Γ `i≡j:γ
Γ ` i1 ≡ j1 : γ1

Γ ` λa. i ≡ λb. j : γ1 Nm
→ γ2
(Γ ).1, a : γ2 ` i1 : γ
(Γ ).1 ` i2 : γ2
Γ ` [i2 /a]i1 ≡ j : γ
Γ ` (λa. i1 )i2 ≡ j : γ

Γ ` i2 ≡ j2 : γ2

Γ ` i1 (i2 ) ≡ j1 (j2 ) : γ2

Eq-β

Γ ` ∅ ≡ ∅ : NmSet

Γ ` M ≡ N : Nm
Γ ` {M} ≡ {N} : NmSet

Eq-App

Eq-Empty

Eq-Single

Γ ` Y1 ≡ Y2 : NmSet

Γ ` (X1 ⊥ Y1 ) ≡ (X2 ⊥ Y2 ) : NmSet
Γ ` (X2 ⊥ X1 ) ≡ Y : NmSet
Γ ` (X1 ⊥ X2 ) ≡ Y : NmSet
Γ ` M ≡ N : Nm Nm
→ Nm

Eq-Pair

Γ ` i1 ≡ j1 : γ1 Nm
→ γ2
Γ ` i2 ≡ j2 : γ1

Eq-Lam

Γ ` X1 ≡ X2 : NmSet

E-Refl

E-Sym

Γ ` (i1 , i2 ) ≡ (j1 , j2 ) : γ1 ∗ γ2

Γ, a ≡ b : γ1 ` i ≡ j : γ2

(Γ ).2 ` i : γ

Γ `i≡i:γ

Eq-Apart

Eq-Perm

Γ ` X ≡ Y : NmSet

Γ ` M[X] ≡ N[Y] : NmSet

Eq-Map

Fig. 28. Deductive rules for showing that two index terms are equivalent

74

Γ `i⊥j:γ

The index terms i and j are apart at sort γ

(a ⊥ b : γ) ∈ Γ
Γ `a⊥b:γ
Γ ` i1 ⊥ j1 : γ1
Γ ` (i1 , i2 ) ⊥ (j1 , j2 ) : γ1 ∗ γ2

Γ `j⊥i:γ

Var

D-Proj1

Γ `i⊥j:γ

Γ ` i2 ⊥ j2 : γ2
Γ ` (i1 , i2 ) ⊥ (j1 , j2 ) : γ1 ∗ γ2

Γ, (a ≡ b : γ1 ) ` i ⊥ j : γ2
Γ ` λa. i ⊥ λb. j : γ1 Nm
→ γ2
Γ ` i1 ⊥ j1 : γ1 Nm
→ γ2

Γ ` i2 ≡ j2 : γ1

D-App

(Γ ).1 ` i2 : γ2
(Γ ).1, a : γ2 ` i1 : γ

Γ ` (λa. i1 )i2 ⊥ j : γ
(Γ ).2 ` X : NmSet
Γ ` ∅ ⊥ X : NmSet

D-Empty

Γ ` X1 ⊥ Y : NmSet

Γ ` M ⊥ N : Nm Nm
→ Nm

D-β

Γ ` M ⊥ N : Nm
Γ ` {M} ⊥ {N} : NmSet
Γ ` X2 ⊥ Y : NmSet

Γ ` (X1 ⊥ X2 ) ⊥ Y : NmSet

D-Single

D-Apart

Γ ` X ≡ Y : NmSet

Γ ` M[X] ⊥ N[Y] : NmSet

D-Proj2

D-Lam

Γ ` i1 (i2 ) ⊥ j1 (j2 ) : γ2
Γ ` [i2 /a]i1 ⊥ j : γ

D-Sym

D-Map

Fig. 29. Deductive rules for showing that two index terms are apart

75

H

Strong Normalization Proof for the Name Term Language

Definition 11 (Rγ (e)).
Nm
1. Rγ (e) if and only if e halts, and γ 6= (γ1 →
γ2 )
2. R(γ Nm
(e)
if
and
only
if
(1)
e
halts
and
(2)
Rγ1 (e 0 ) implies Rγ2 (e e 0 ).
→γ )
1

2

Lemma 21 (Termination). If Rγ (e), then e halts.
Proof. By definition of Rγ (e).
Lemma 22 (Preservation). If Γ ` e : γ and σ ` Γ , then ` [σ]e : γ.
Proof. By induction on the size of σ. When size(σ) = 1, the Lemma reduces to
the Substitution Lemma.
Lemma 23 (Normalization). If Γ ` e : γ and σ ` Γ , then Rγ ([σ]e).
Proof. By induction on the given derivation.
Case
Γ ` () : 1

M-unit

[σ]() = ()
By definition of [σ](−)
() ⇓M ()
By Rule teval-value
[σ]() ⇓M ()
Since [σ]() = (), () ⇓M ()
Γ ` () : 1
Given
` [σ]() : 1 By Lemma 22 (Preservation)
Z
R1 ([σ]()) Since [σ]() ⇓M ()
and ` [σ]() : 1
Case
Γ ` n : Nm

M-const

Similar to the M-unit case.
Case (a : γ) ∈ Γ
M-var
Γ `a:γ
∃vi .([σ]a ⇓M vi )
By definition of [σ](−)
` [σ]a : γ From Lemma 22 (Preservation)
Z
Rγ ([σ]a) Since [σ]a ⇓M vi
and ` [σ]a : γ
Case

Γ, a : γ1 ` M : γ2
Nm
Γ ` (λa. M) : (γ1 →
γ2 )

M-abs

76

[σ, a → γ1 ] ` Γ 0
Assumption, where Γ 0 = Γ, a : γ1
Nm
` ([σ, a → γ1 ](λa. M)) : (γ1 → γ2 ) By Lemma 22 (Preservation)
[σ, a → γ1 ](λa. M) = (λa. M)
By definition of [σ](−)
Z Rγ ([σ, a → γ1 ](λa. M))
Since [σ, a → γ1 ](λa. M) ⇓M (λa. M)
Nm
and ` [σ, a → γ1 ](λa. M) : (γ1 →
γ2 )
Case

Nm
γ)
Γ ` M2 : γ 0
Γ ` M1 : (γ 0 →
M-app
Γ ` (M1 M2 ) : γ

([σ]M1 )
R(γ 0 Nm
→ γ)

By inductive hypothesis

Rγ 0 ([σ]M2 )
By inductive hypothesis
Rγ (([σ]M1 [σ]M2 )) By definition of R− (−)
Z Rγ ([σ](M1 M2 )) By definition of [σ](−)
Case Γ ` M : γ
Γ ` M2 : γ2
1
1
M-pair
Γ ` (M1 , M2 ) : (γ1 × γ2 )

∃v1 .([σ]M1
∃v2 .([σ]M2
([σ]M1 , [σ]M2 )
[σ](M1 , M2 )
Z

Case

Rγ1 ([σ]M1 )
By inductive hypothesis
Rγ2 ([σ]M2 )
By inductive hypothesis
⇓M v1 )
Since Rγ1 ([σ]M1 )
⇓M v2 )
Since Rγ2 ([σ]M2 )
⇓M (v1 , v2 )
By Rule teval-tuple
⇓M (v1 , v2 )
By definition of [σ](−)
` [σ](M1 , M2 ) : (γ1 × γ2 ) From Lemma 22 (Preservation)
R(γ1 ×γ2 ) ([σ](M1 M2 )) Since [σ](M1 M2 ) ⇓M (v1 , v2 )
and ` [σ](M1 M2 ) : (γ1 × γ2 )

Γ ` M1 : Nm
Γ ` M2 : Nm
M-bin
Γ ` hhM1 , M2ii : Nm

∃v1 .([σ]M1
∃v2 .([σ]M2
hh[σ]M1 , [σ]M2ii
[σ]hhM1 , M2ii
Z

RNm ([σ]M1 )
By inductive hypothesis
RNm ([σ]M2 )
By inductive hypothesis
⇓M v1 )
Since Rγ1 ([σ]M1 )
⇓M v2 )
Since Rγ2 ([σ]M2 )
⇓M (v1 , v2 )
By Rule teval-bin
⇓M (v1 , v2 )
By definition of [σ](−)
` [σ]hhM1 , M2ii : Nm From Lemma 22 (Preservation)
RNm ([σ]hhM1 , M2ii) Since [σ]hhM1 , M2ii ⇓M (v1 , v2 )
and ` [σ]hhM1 , M2ii : Nm

77

Theorem 6 (Strong Normalization). If Γ ` e : γ, then e is normalizing.
Proof.
Rγ (e) By Lemma 23 (Normalization)
Z e halts By Lemma 21 (Termination)

I

Strong Normalization Proof for the Index Term Language

Definition 12 (Rγ (e)).
1. RNmSet (e) iff e halts.
2. R(γ Nm
(e) if and only if (1) e halts and (2) if Rγ1 (e 0 ) then Rγ2 (e e 0 ).
→γ )
1

2

3. Rγ1 ×γ2 (e) if and only if e halts and Rγ1 (e) and Rγ2 (e).
Lemma 24 (Termination). If Rγ (e), then e halts.
Proof. By definition of Rγ (e).
Lemma 25 (Preservation). If Γ ` e : γ and σ ` Γ , then ` [σ]e : γ.
Proof. By induction on the size of σ. When size([σ]) = 1, the Lemma reduces to
the Substitution Lemma.
Lemma 26 (Normalization). If Γ ` e : γ and σ ` Γ , then Rγ ([σ]e).
Proof. By induction on the given derivation.
Case (a : γ) ∈ Γ
sort-var
Γ `a:γ
∃vi .([σ]a ⇓ vi )
By definition of [σ](−)
` [σ]a : γ By Lemma 25 (Preservation)
Z
Rγ ([σ]a) Since [σ]a ⇓M vi and ` [σ]a : γ
Case
Γ ` () : 1

sort-unit

[σ]() = ()
By definition of [σ](−)
() ⇓ ()
By Rule value; Since () val
[σ]() ⇓ ()
Since [σ]() = (), () ⇓ ()
Γ ` () : 1
Given
` [σ]() : 1 By Lemma 25 (Preservation)
Z
R1 ([σ]()) Since [σ]() ⇓ () and ` [σ]() : 1

78

Case Γ ` i : γ
Γ ` i2 : γ2
1
1
sort-pair
Γ ` (i1 , i2 ) : (γ1 × γ2 )

∃v1 .([σ]i1
∃v2 .([σ]i2
([σ]i1 , [σ]i2 )
[σ](i1 , i2 )
Z

Rγ1 ([σ]i1 )
By inductive hypothesis
Rγ2 ([σ]i2 )
By inductive hypothesis
⇓ v1 )
Since Rγ1 ([σ]i1 )
⇓ v2 )
Since Rγ2 ([σ]i2 )
⇓ (v1 , v2 )
By Rule pair
⇓ (v1 , v2 )
By definition of [σ](−)
` [σ](i1 , i2 ) : (γ1 ∗ γ2 ) By Lemma 25 (Preservation)
R(γ1 ∗γ2 ) ([σ](i1 i2 )) Since [σ](i1 i2 ) ⇓ (v1 , v2 )
and ` [σ](i1 i2 ) : (γ1 × γ2 )

Case Γ ` i : γ ∗ γ
1
2
sort-proj
Γ ` prjb i : γb
R(γ1 ∗γ2 ) ([σ]i) By inductive hypothesis
Rγb ([σ] prjb i) By definition of R− (−)
Case
Γ ` ∅ : NmSet

sort-empty

Similar to the sort-unit case.
Case
Γ ` N : Nm
sort-singleton
Γ ` {N} : NmSet
[σ]{N} = {N}
By definition of [σ](−)
{N} val
By Rule val-singleton
Γ ` {N} : NmSet Given
` [σ]{N} : NmSet By Lemma 25 (Preservation)
Z
RNmSet ([σ]{N}) Since [σ]{N} val, ` [σ]{N} : NmSet
Case

Γ ` X : NmSet
Γ ` Y : NmSet
sort-union
Γ ` (X ∪ Y) : NmSet

RNmSet ([σ]X)
By inductive hypothesis
RNmSet ([σ]Y)
By inductive hypothesis
∃v1 .([σ]X ⇓ v1 )
Since RNmSet ([σ]X)
∃v2 .([σ]Y ⇓ v2 )
Since RNmSet ([σ]Y)
([σ]X ∪ [σ]Y) ⇓ (v1 ∪ v2 )
By Rule union
[σ](X ∪ Y) ⇓ (v1 ∪ v2 )
By definition of [σ](−)
` [σ](X ∪ Y) : (NmSet) By Lemma 25 (Preservation)
Z RNmSet ([σ](X ∪ Y)) Since [σ](X ∪ Y) ⇓ (v1 ∪ v2 )
and ` [σ](X ∪ Y) : NmSet

79

Case Γ ` X : NmSet
Γ ` Y : NmSet
extract(Γ ) X ⊥ Y : NmSet
sort-sep-union
Γ ` (X ⊥ Y) : NmSet

∃v1 .([σ]X
∃v2 .([σ]Y
([σ]X ⊥ [σ]Y)
[σ](X ⊥ Y)
Z
Case

RNmSet ([σ]X)
By inductive hypothesis
RNmSet ([σ]Y)
By inductive hypothesis
⇓ v1 )
Since RNmSet ([σ]X)
⇓ v2 )
Since RNmSet ([σ]Y)
⇓ (v1 ⊥ v2 )
By Rule union
⇓ (v1 ⊥ v2 )
By definition of [σ](−)
` [σ](X ⊥ Y) : (NmSet) By Lemma 25 (Preservation)
RNmSet ([σ](X ⊥ Y)) Since [σ](X ⊥ Y) ⇓ (v1 ⊥ v2 )
and ` [σ](X ⊥ Y) : NmSet

Γ, a : γ1 ` i : γ2
idx
Γ ` (λa. i) : (γ1 →
γ2 )

sort-abs

[σ, a → γ1 ] ` Γ 0
Assumption, where Γ 0 = Γ, a : γ1
idx
` ([σ, a → γ1 ](λa. i)) : (γ1 → γ2 ) By Lemma 25 (Preservation)
[σ, a → γ1 ](λa. i) = (λa. i)
By definition of [σ](−)
Z Rγ ([σ, a → γ1 ](λa. i)) Since [σ, a → γ1 ](λa. i) ⇓ (λa. i)
idx
and ` [σ, a → γ1 ](λa. i) : (γ1 →
γ2 )
Case

idx
Γ ` i : γ1 →
γ2
Γ ` j : γ1
sort-apply
Γ ` i(j) : γ2

R(γ

idx
1 →γ2 )

([σ]i) By inductive hypothesis

Rγ1 ([σ]j)
By inductive hypothesis
Rγ2 (([σ]i([σ]j))) By definition of R− (−)
Z Rγ2 ([σ](i(j))) By definition of [σ](−)
Case

Nm
Γ ` M : Nm →
Nm
Γ ` j : NmSet
sort-map-set
Γ ` M[j] : NmSet

RNmSet (j) By inductive hypothesis
∃v.(M[j] ⇓ v)
By Thm. 6
∃v 0 .(M[j] ; v)
By Rule Single
M[j] ⇓ v 0
By Rule map-set
` ([σ](M[j]) : NmSet By Lemma 25 (Preservation)
Z RNmSet ([σ](M[j]) Since M[j] = v 0 and ` ([σ](M[j]) : NmSet

Theorem 7 (Strong Normalization). If Γ ` e : γ, then e is normalizing.

80

Proof.
Rγ (e) By Lemma 26 (Normalization)
Z e halts By Lemma 24 (Termination)

