A type theory for memory allocation and data layout.
Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We show that a language based on ordered types can use this property to give an exact account of the layout of data in memory. The fuse constructor from ordered logic describes adjacency of values in memory, and the mobility modal describes pointers into the heap. We choose a particular allocation model based on a common implementation scheme for copying garbage collection and show how this permits us to separate out the allocation and initialization of memory locations in such a way as to account for optimizations such as the coalescing of multiple calls to the allocator.
Introduction
High-level programming languages such as ML and Java allow programmers
to program in terms of abstractions such as pairs, records,
and objects, which have well-defined semantics but whose realizations
in terms of the underlying concrete machine are left unspecified
and unobservable.
Sometimes, it is necessary to program without these abstractions.
. A programmer may need to interact with an operating system
or a network or another programming language in such a way
as to require exact knowledge of, and control over, the manner
in which data is laid out in memory.
. A compiler must choose a concrete implementation for
the high-level abstractions provided by the source level
language-such as the actual layout of data in memory and
the manner in which such memory gets allocated and initialized

Traditionally, both of these needs have been addressed in an un-
typed, or a weakly typed fashion. Languages such as C give programmers
relatively precise control over data layout and initialization
at the expense of type and memory safety. Traditional compilers
represent programs internally using un-typed languages, relying
on the correctness of the compiler to preserve any safety properties
enjoyed by the source program.
Recently, research in the areas of typed compilation and certified
code [12, 21, 11] has focused on providing type systems for low-level
languages in which abstractions such as control flow and data
layout are made explicit. These ideas have been used in a number of
compilers [12, 21, 9, 2, 19, 6]. However, some of the mechanisms
that have been invented to describe low-level operations are fairly
ad hoc and do not yet have an interpretation in standard type the-
ory. For example, in the typed assembly language formalism[11],
allocation and initialization can be separated, but at the expense of
having to annotate each type with a flag indicating whether or not
the value it classifies has been initialized. This kind of low-level
technique seems unlikely to integrate well with a high-level programming
language.
In this paper, we attempt to give a type theoretic account of data
layout that provides a foundation for defining how high-level constructs
such as pairs are laid out in memory. We realize our system
with a concrete allocation model based on a common implementation
of a copying garbage collector and show that we can separate
out the process of allocating a block of memory from the process
of initializing the individual memory words. Our system is flex-
2.3. 3 4 5
1.

Figure

1. Three possible layouts for the term (3,(4,5))
ible enough to permit multiple allocation calls to be coalesced so
that memory for multiple source level objects can be allocated si-
multaneously, while ensuring that calls to the allocator can never
invalidate assumptions made about the state of partially initialized
data.
An important contribution of this work is that it remains completely
within the framework of a lambda calculus which enjoys the standard
meta-theoretic properties. In this way, we reconcile the very
low-level notion of allocated memory with the substitution properties
expected of a high-level programming language. This is of particular
interest because it suggests the possibility that these ideas
could be made available to programmers, so that even programs
requiring detailed control of memory layout could be written in a
high-level language.
2 Data layout and allocation
Specifying the layout of data in memory is an essential part of realizing
a high-level program as a concrete collection of machine instructions
and data, but one which is usually not of direct interest to
programmers. The programmer cares about the ability to construct
objects, but most of the time cares about the layout in memory only
insofar as it affects the performance of operations on an object.
How terms should be laid out in memory is therefore a matter of
policy for the compiler writer. For example, the lambda calculus
term (3,(4,5)) of type int- (int-int) defines a pair whose first
element is 3 and whose second element is a pair containing 4 and 5.

Figure

shows several possible representations for this term. One
compiler might choose to represent this as a pointer to a pair, whose
elements are an integer and a pointer to another pair. However,
another might choose to add an indirection to integers, or to attempt
to flatten the whole term into three adjacent cells in memory.
The high level notion of pairing captures certain operational properties
that are useful to the programmer, but does not uniquely specify
an implementation strategy. Commonly, a compiler simply chooses
to interpret the pair type as meaning one particular strategy. For the
purposes of giving a general account of data layout, this is clearly
unsatisfactory as it does not permit us to break the high-level concept
into its constituent concepts.
A first step to a more general type theory for data layout is to observe
that there seem to be two key concepts used by the different
interpretations of pairing given in figure 1: adjacency and indirec-
tion. Each of the different choices of representation corresponds to
a different choice as to which data is to be represented by physically
adjacent bytes in memory and which data is to be represented
via an indirection into another portion of memory. This is the first
notion that we shall attempt to capture in our type system.
2.1 Allocation
Once the layout of data in memory has been made explicit, it becomes
possible to consider the process by which new memory is
created and initialized. We suggest that it is useful to think of this
in terms of three stages, regardless of the mechanism employed.
Reservation is the process by which a new block of uninitialized
memory is created.
Initialization is the process by which values get written into the
reserved memory, potentially changing its type. It is important
for type safety that either the memory be treated linearly in
this stage, or else that the initialization operations be such that
they only refine the type [3].
Allocation is the process by which a section of reserved (and presumably
initialized) memory is made available as an ordinary
unrestricted object.
Different memory-management systems combine these stages in
different ways. For example, in the TAL framework [11], reservation
and allocation are done atomically, and hence initialization
is very restricted in how it can change the type.
The concrete memory management system that we choose to model
is one commonly used in practice by copying garbage collectors
and hence is of particular interest. This choice is not essential-
other systems can be expressed using similar techniques to those
we present here.
In a copying garbage collector, the available memory can be divided
into two adjacent contiguous sections: a heap containing data that
has been allocated since the last garbage collection (or perhaps just
the youngest generation thereof), and a possibly empty freespace
containing memory that has not yet been allocated. The allocator
maintains an allocation pointer (or freespace pointer), which points
to the end of the allocated data and the start of the free memory, and
a heap-limit pointer, which points to the end of the free memory.
To create a new heap object requiring n bytes, the program first
compares the allocation pointer to the heap-limit pointer to ensure
that there are at least n bytes available in the freespace. If not, it
calls the garbage collector to free up enough space. This step corresponds
to the reservation phase discussed above. Once sufficient
memory has been found-either in the existing freespace or by calling
the garbage collector-the program may assume that n bytes of
space exist in front of the allocation pointer. We refer to this
initialized area as the frontier.
Once space has been reserved on the frontier, values can be written
into the individual cells of memory via offsets from the allocation
pointer. This corresponds to the initialization phase.
At any point, the program may "move" a prefix of the frontier into
the heap. The value of the allocation pointer becomes the pointer to
the new heap value, and the allocation pointer is advanced past the
allocated space. This corresponds to the allocation phase.

Figure

2 gives an example of this process. The first line shows a
schematic diagram of the heap and the freespace, where a.p. stands
for the allocation pointer and l.p. stands for the limit pointer. The
heap freespace
l.p.
a.p.
d := x
c := 3
freespace
x5heap
l.p.
a.p.
x y
reserve 4 as [a,b,c,d]
a := 4
a b c d
l.p.
a.p.
freespace
d
c
heap
l.p.
a.p.
x
freespace

Figure

2. Reservation, initialization, and allocation of (3,(4,5))
ragged boundary of the freespace indicates that we have no information
about its extent-it may potentially be exhausted.
The second line of the figure shows the result of reserving four
words of space-sufficient for allocating the term (3,(4,5)) using
the first layout strategy from Figure 1. We refer to the individual
cells of the frontier by the names a,b,c and d. Note that this step
may have invoked the garbage collector to free up more memory if
the freespace from the previously line was in fact exhausted.
To create the pair (4,5) we assign 4 to a, 5 to b, and then allocate
a and b into the heap getting back a heap pointer x as shown on the
third line of the figure. We can then initialize the top-level pair by
writing 3 to c and x to d. A final allocation step gives us a pointer
y which refers to a heap allocated structure of the form pictured in
the first line of Figure 1.
As this example shows, we do not require that the entire frontier be
allocated as a single object. The program may choose to reserve
space for several objects at once and then initialize and allocate
them individually. This optimization avoids multiple checks against
the heap-limit pointer.
There are two constraints on this process that must be captured by
our type system to ensure safety.
Firstly, the manner in which we "move" objects into the heap means
that objects cannot be allocated from the middle or end of the fron-
tier. Only prefixes of the frontier-that is, contiguous blocks of
memory adjacent to the allocation pointer-may be allocated.
Secondly, reserved space in the frontier cannot persist across successive
reservations nor across function calls. When the garbage
collector is called it will copy the live data to a new heap and change
the allocation pointer to point to this new location. Any partially
initialized data that was previously in the frontier will be lost in the
process.
This corresponds to a kind of destructive effect: the state of the
frontier cannot be assumed to be preserved across the evaluation
of any term that could potentially call the allocator. The type system
must therefore ensure that no assumptions about the state of
the frontier can persist across the evaluation of any term that might
reserve or allocate memory.
3 Ordered linear type theory
Ordered (or non-commutative) linear logic is a variant of standard
linear logic in which hypotheses must not only be used exactly
once, but must also be used in order [17, 16, 18, 15]. The corresponding
proof terms make up an ordered lambda calculus that is
characterized by the lack of an exchange property for the ordered
context in addition to the usual linearity restrictions. We present
a small fragment of the ordered lambda calculus by way of introduction
to the these ideas. The presentation here is simpler than
previous work, in that it omits the linear context, retaining only the
ordered and unrestricted contexts. The modal therefore moves directly
from the ordered terms to unrestricted terms.
Typing rules for the ordered lambda calculus have the form G;W #
t, indicating that the M has type t under the variable assumptions
declared in the unrestricted context G and the ordered context
W. We distinguish syntactically between ordered variables a
which must be used linearly and in order, and unrestricted variables
x which may be used arbitrarily often.
Unlike standard linear type theory, the ordered comma operator
interpreted as simple list concatenation and does not permit
the intermingling of hypotheses. Where unambiguous, we write
a:t instead of a:t, - for singleton contexts.
unrestricted arrow
multiplicative
unrestricted contexts
| x unrestricted variables
| n integer literals
| M .M fuse intro
| leta 1 .a 2 =MinM fuse elim
| l(x:t).E lambda intro
| M M lambda elim

Figure

3. Standard ordered lambda calculus syntax
This definition means that concatenation of contexts preserves the
order of the entries in the contexts.
The multiplicative connective (fuse) demonstrates a use of this concatenation
operator.
The elimination rule for fuse splits it into components and places
them in the ordered context. Notice that the variables representing
the components of M 1 go into the ordered context in place of W.
Finally, the mobility modal permits terms that are orderedly closed
to be moved to the unrestricted context.
G;
G;
3.1 Size preservation and adjacency
There are three interesting observations that we can make about
ordered lambda calculus terms that motivate the application of ordered
type theory to data layout.
1. Because ordered variables may not exchange position in the
context, we may think of ordered variables as simply standing
for locations in the ordered context.
2. We may break ordered terms down into their components and
re-form them, but we may not change their order. In particu-
lar, the term that splits apart an ordered pair and reforms it in
the opposite order is not well-typed.
let a 1 .a a in a 2 .a 1
Viewed as a linear (rather than ordered) term, this code would
be well-typed.
3. The ! modality takes an ordered term whose location is fixed
and moves it into the unrestricted context, where its location
become indeterminate.
Based on these observations, we propose the following three intuitions
as the basis for our system.
1. An ordered context may be thought of as describing a particular
region of memory under consideration. Ordered variables
correspond to locations, or offsets into the region. Adjacent
variables in the context correspond to physically adjacent lo-
cations, with extents given by the types of the variables.
2. The fuse constructor t 1 .t 2 describes terms that are physically
adjacent in memory. The fact that we cannot reorder ordered
terms corresponds naturally to the fact that we cannot reorder
bytes in memory.
3. The ! modality ! t corresponds to an indirection out of the region
of memory described by the ordered context into another
(unspecified) part of the heap.
The standard ordered lambda calculus does not entirely justify these
intuitions. Ordered terms preserve the order of sub-components,
but they do not in general preserve their adjacency. The essence of
this problem can be seen in the derived ordered substitution principle

Notice that the portion of the ordered context that is passed to the
term being bound is replaced with the variable itself when type-checking
the rest of the body. Our intention is that operations such
as this should be done in-place on the memory described by the ordered
context. However, the following term demonstrates that this
does not hold in the general ordered lambda calculus.
G;
The problem is that we are able to insert unrestricted terms into the
ordered terms in arbitrary places. While this does not violate our
notion that ordered variables correspond to locations, it does mean
that these locations are not fixed. Operationally, it would seem that
we would be forced to shift all of W 2 over in memory to make room
for the new term in the context.
An alternative way of looking at this is that the general ordered
lambda calculus is not size preserving: the sub-derivation G:- #
produces a term of size one from a context of size zero.
If we interpret the ordered context as describing a region of mem-
ory, then the above term inserts a word-sized value into an empty
region of memory! In order to prevent such problematic terms, it
is necessary to carefully restrict the calculus in such a way as to
ensure that operations on memory preserve size.
The notion of size preservation is the last insight necessary to formulate
a lambda calculus in which we can give a full account for
data layout. We will use the fuse type to describe adjacency and
the modal type to describe indirection, while restricting the terms
in such a way as to enforce various key size preservation properties.
The allocation model described in section 2 will be accounted for by
using an ordered context to describe the frontier. Ordered variables
then become offsets into the frontier, and reservation, initialization,
and allocation become operations on ordered terms. The linearity of
ns | n | V .V | l(x:t).E | !V
ns | n | l(x:t).E | !V
| reserve n as ain E | alloc Q as xin E
|
| let
| let
| let! (x . x) =M in E | let ! x =M in E

Figure

4. Syntax
the ordered context will permit destructive operations on the frontier
(such as initialization), and the size preservation property will
ensure that all operations on the frontier may be done in-place.
4 The orderly lambda calculus
We now have all of the ideas that we need to define a language for
data layout and allocation, which we shall call the orderly lambda
calculus, or l ord for short. For the sake of brevity, this paper will
focus on a small core language that captures the essential ideas.
The syntax of the core language is given in figure 4. We use the
notation t n for an n-ary fuse of t.
For data layout purposes, we only require a few new types from
the ordered lambda calculus: the fuse constructor which models
adjacency; the modal constructor, which models indirection; and
the multiplicative unit. Other types include a base type of integers
and the type of unrestricted functions. The NS (nonsense) type is
the type of a single un-initialized word of memory.
It is important for our purposes to distinguish between types which
are of unit size and hence can be kept in registers or on the stack,
and other types that must be heap allocated. This is accomplished
by a kinding distinction k. The kind T reg classifies the types
of values which may be loaded into registers, whereas the kind T h
classifies types that may be heap-allocated (a strict super-set of the
former).
An important property of this language is that types uniquely determine
the size of the data they classify.
For simplicity, the smallest unit of size we consider is a single machine
word. The multiplicative unit type has size zero, since it is
inhabited by a single value which therefore does not need to be rep-
resented. We view the function type as having unit size, since we
expect that a practical implementation would use closures to represent
functions. Under closure conversion, lambdas become existentially
quantified records allocated on the heap, and hence are
represented by a pointer of unit size. We assume that the actual
code for the function will be statically allocated.
Ordered contexts W map ordered variables a to types t, and are
used to describe regions of memory (in particular, the frontier). The
notion of sizing for types extends naturally to ordered contexts.
As before, exchanging, discarding, or duplicating variables in the
ordered context is not permitted.
Unrestricted contexts G map ordinary variables x to their types. The
well-formedness judgement for unrestricted contexts checks that all
unrestricted variables have unit-sized types-that is, types whose
kind is T reg . Ordinary variables correspond to registers or stack slots
in the underlying machine, and so are restricted to have word size
via this kinding mechanism. This is a key point about the orderly
lambda calculus: all large objects are required to be explicitly allocated
and initialized.
The term level of l ord is split into four separate syntactic classes:
coercion terms Q, heap values V , terms M and expressions E. The
main typing judgements are described in figure 5, along with comments
about the size properties which they enjoy. Complete definitions
of the typing rules can be found in appendix A.
Making allocation explicit introduces a kind of effect into the lan-
guage. Reserving and allocating memory is an effectful operation,
and as we saw in the previous section these effects may interfere.
In order to control these effects and their interaction we introduce
a distinction between terms M and expressions E in the style of
Pfenning and Davies [14], but without an explicit modal type for
computations. (The computation type does not seem useful in our
setting since we do not have the inclusion of expressions into terms,
instead taking the partial arrow as primitive).
The syntactic form we impose is not overly restrictive: it is actually
related to, but more permissive than, the A-normal or CPS forms
that many compilers typically use.
4.1 Terms
Terms M correspond to values that do not reserve or allocate in
the course of their evaluation, but that may contain free references
to ordered variables (that is, to the frontier). In this presentation,
all terms are values-but it is straightforward and useful to include
other primitive operations that do not allocate (such as integer oper-
ations) at this level. The typing judgement for terms is of the form
t. The term M may refer to variables in G arbitrarily
often, but must refer to each variable in W exactly once, and in an
ordered fashion.
The typing rules for terms are for the most part unsurprising. For
the l-abstraction case, the body of the function is checked as an
expression, with the argument placed in the unrestricted context.
Notice that we permit free references to the frontier in functions.
Since function application lies in the category of expressions, we
Judgement Size properties Meaning
# W W is a well-formed ordered context.
is a well-formed unrestricted context.
is a well-formed type.
to look like t .
is a non-allocating/non-reserving term of type t.
typed expression of type t which consumes W.
is a closed value of type t.
well-typed frontier for the ordered context W.

Figure

5. Typing judgements for l ord
will defer discussion of the elimination form to Section 4.4. All
other terms must be closed with respect to the ordered context.
The most non-standard term is !V . This term corresponds to a
pointer into the heap to a location occupied by the heap value V ,
and is the canonical form for terms of type ! t.
G; - # trm
An interesting facet of our presentation is that we account for heap
allocation without requiring an explicit heap (for example in the
style of Morrisett and Harper [10]). In a heap semantics, a pointer
to a value V is represented by a label #, with # bound to V in an explicit
heap data-structure. Since sharing is not observable in our
simple calculus, we avoid this extra complexity by representing
such values directly as !V , denoting a pointer to a location occupied
by V . We stress that this is purely a technical convenience-it
is straightforward to give a heap semantics in which the sharing is
made explicit in the usual fashion.
4.2 Heap Values
may occur in memory. It is
therefore essential that they be closed. An open heap term would
require that a new copy be implicitly allocated every time different
values were substituted into it, which is contrary to the aims of
l ord . The typing judgement for heap values, # val t, enforces this
property.
The primary motivation for having heap values comes from the operational
semantics of the language. However, it is not intended
that they should play the role of so-called "semantic objects" that
are only permitted to be introduced in the course of evaluation. It is
perfectly reasonable for a programmer to write heap values in the
source program. Doing so corresponds precisely to the notion of
statically allocated data-that is, data that is present in the heap at
the start of the program.
The important difference between heap values and terms is that
heap values may be of arbitrary size. This is reflected in the syntax
by the value denoting a contiguous block of memory in
which V 1 is laid out adjacent to the value V 2 .
The fact that fused terms are adjacent means that the . constructor
is associative in the sense that the term 3. (4 .5) has the same
representation in memory as the term (3 . 4) . 5. Both terms describe
three successive words of memory, occupied by the integers
3, 4, and 5 respectively. This is a fundamental difference from ordinary
lambda calculus pairing, in which (3,(4,5)) is almost certain
to have a different representation from ((3,4),5).
This associativity is just one example of values which have different
types but the same representations. Other examples include values
involving the ordered unit, #. Since we do not choose to represent
this value, we expect that the representations of 3 . 3, and 3
will all be the same at runtime.
Coercion terms exist to provide a mechanism by which to convert
between such values which have different typing structure but the
same underlying representation.
4.3 Coercions
The level of coercion terms in this fragment of the language is extremely
simple, consisting only of variables a, the ordered unit #,
and fuse Q 1 .Q 2 . Coercion binding and elimination forms are provided
at the expression level (Section 4.4).
Intuitively, coercion terms package up the frontier into new forms
without changing the underlying representation. For example, the
term a 1 . a 2 takes the section of the frontier described by a 1 and
the section described by a 2 and combines them into a single fuse
which could then be bound at a new name using the expression
level coercion let. The orderedness of the terms ensures that the
two sections were already adjacent, and hence combining them into
a fuse does not change their representation.
The typing judgement for coercion terms is of the form W # crc
signifying that Q re-associates W to have the form t. The coercive
nature of the terms is exhibited in the size preservation property that
holds of this judgement: that
The unit term is well-typed in the empty context.
4.4 Expressions
So far we have only seen the value forms that occupy or coerce
memory, but that do not modify it. The memory operations-
reservation, allocation, and initialization-are all done at the level
of expressions.
The well-formedness judgement for expressions is given by
t. The ordered context W in the typing judgement describes
the current state of the frontier. Because of the destructive
nature of the reserve and allocate operations, the interpretation is
that the frontier is consumed by the expression E. That is, any
space that is on the frontier must either be allocated by E, or explicitly
destroyed.
As we saw in section 2, memory operations are effectful, and so
the type system for expressions must be carefully designed to ensure
that these effects do not interfere. This is enforced by always
passing the entire ordered context (and hence the entire frontier) to
each sub-expression (but not sub-term). In this way, we ensure that
every possibly allocating/reserving expression has a correct view of
the entire frontier when it is evaluated.
The expressions can be conceptually divided into four basic categories

Ordinary expressions
The inclusion of values into expressions is given by the expression
retM.
G;
G;
This is the only value form for expressions, and consumes no re-
sources. It is unsound to permit the term M to contain ordered vari-
ables, since it may be substituted for an unrestricted variable by the
primitive let form discussed below.
Function application is an expression, since the evaluation of the
body of the function may engender memory effects. Applications
are syntactically restricted to permit only application of a term to
another term.
G; - # trm
The term being applied is permitted to refer to ordered variables,
but the argument must be closed since unrestricted functions may
duplicate or drop their arguments. Application allows us to define
a term-level let construct with the following derived typing rule.
G;
This let is not fully general, since there is no way to bind the result
of an application to a variable. Therefore, we introduce a primitive
let form to bind expressions to variables.
Notice that we pass the entire ordered context to the first sub-
expression. This is a crucial point: E 1 may have memory effects
that could invalidate any previous assumptions about the state of the
frontier that E 2 might make. Therefore, E 2 cannot assume anything
at all about the state of the frontier-that is, it must be well-typed
in an empty ordered context.
Somewhat surprisingly, it is safe to permit E 1 to have free references
to the ordered context. This is reasonable because expressions
consume resources, but do not contain them. By this we mean
that the value form for expressions (retM) is well-typed only in an
empty ordered context. Therefore, if the ordered context W is not
empty, then E 1 must explicitly destroy or allocate all of the memory
described by W before it reaches a value. Since this value will be
orderedly closed, it is safe to substitute it freely for the unrestricted
variable x.
Memory expressions
The most interesting and non-standard expressions are those dealing
directly with the frontier. Recall that there are three operations
of interest: reserving space on the frontier, initializing pieces of the
frontier, and allocating prefixes of the frontier into the heap. These
three operations are captured directly as primitives. As we shall see
later, this is not entirely necessary-by extending the type system
somewhat we can give types to these primitives as constants. For
simplicity however, we first present them as primitive notions.
The first operation, reservation, discards any resources that were
previously mentioned in the ordered context, and introduces n
words of nonsense into the frontier.
reserve n as
This corresponds exactly to the reservation operation described in
Section 2.1, which destroys any existing data on the frontier and
provides a block of "new" uninitialized space.
Memory must be written using assignment.
G;
The ordered term Q gives the location in the ordered context to
which the value should be written. This location is then referred
to by a in the body of the expression. The linearity of the ordered
context is important here, since we are destructively changing the
type of a memory location.
At any point, space can be allocated from the left side of the frontier
with the alloc construct.
The coercion term Q describes a section of the frontier to be packaged
up as a boxed heap value. The splitting of the ordered context
ensures that the term to be allocated is a prefix of the frontier. The
new heap value is given a pointer type and permitted to be used
unrestrictedly for the rest of the program.
Coercion expressions
The memory expressions manipulate the frontier using ordered
variables, which stand for offsets into the frontier. Coercions are
used to manipulate ordered variables, combining them into bigger
terms or breaking them into smaller pieces.
The simplest coercion expression is the elimination form for unit.
G;
if t is not a fuse and
load t x =M[i] in E
load
load
t is not a fuse

Figure

6. An example of a direct-load defined in terms of split
Since the unit term is considered to have zero size, we may eliminate
it freely from the ordered context without changing the size or
adjacency properties of the terms in the frontier.
The elimination form for fuse is also a coercion expression.
The intuition is that since t 1 . t 2 describes two adjacent blocks of
memory, we are free to view the single block of memory described
by Q as two adjacent blocks at offsets named by a 1 and a 2 .
The last coercion operation is the simple ordered let form, which
permits ordered terms to be packaged up or renamed.
Load expressions
The memory operations account for the creation of heap objects.
Equally important is the ability to load values out of the heap. Once
an object is in the heap, we must have some way of accessing its
components. Pointers to "small" objects can be de-referenced directly

G;
The kinding restriction ensures that the only values that can be
loaded with this operation are those that will fit into a register.
To access the fields of larger objects, we provide a composite elimination
construct that takes a pointer to a large object, and produces
two pointers to the immediate subcomponents of the object.
G;
Notice that the variables are bound not to the components of M
themselves, but rather to pointers to the components of M. Using
this expression we may successively iterate over large composite
objects until we arrive at a pointer to a small object which can be
loaded directly.
This construct is somewhat disturbing from a practical standpoint
for two reasons. In the first place, it seems to require pointers into
the interior of objects (sometimes called locatives) in order to be
implemented efficiently. While not completely out of the question,
interior pointers can be quite problematic for copying garbage collectors
(at least when implemented as direct pointers into the interior
of heap objects).
More importantly however, this construct does not permit constant
time access to fields of a heap-allocated record. For example, to
access the last element of a n-ary tuple in right-associated form requires
computations before we arrive at a term that can be loaded
directly. This is clearly impractical.
We choose to use this "split" operation as the primitive notion because
it provides a simple and natural elimination form. In practice
however, it is likely that this term would be eliminated in favor of
one of a number of direct-load constructs that are definable in terms
of split (figure 6). By taking such a direct-load as primitive and giving
it a direct implementation, the need for the interior pointers is
eliminated and fields of records can be loaded in constant time.
4.5 Frontier semantics
In order to make the connection between the orderly lambda calculus
and the frontier model of allocation clear, the semantics keeps
an explicit frontier. This means that the reduction relation is defined
not just on expressions, but rather on a frontier and an expression
together.
Frontier terms w (as defined in figure (that
is, offsets) to values V . From the standpoint of the operational se-
mantics, the frontier plays a role very similar to an explicit substi-
tution. The typing judgement for the frontier, # w : W, asserts that
the ordered context W describes a frontier that looks like w.
The evaluation relation for the orderly lambda calculus is given in
terms of frontier/expression pairs.
The relation (w,E) # (w # , indicates that in frontier w, the expression
reduces in a single step to the expression E # , with new
frontier w # . The complete definition of this relation is given in Appendix
B.
It is straightforward to show that reduction preserves typing, and
that well-typed terms that are not values may always be reduced
further.
Theorem 1 (Progress & Preservation)
1. Either (w,E) # (w # ,
2. if (w,E) # (w # ,
PROOF. The proof proceeds by induction on the derivation of
t, with the help of several substitution lemmas and some
auxiliary lemmas proving properties of ordered contexts and frontiers

4.6 Size properties
An important property of the orderly lambda calculus is that types
uniquely determine the size of the data that they represent. We have
informally mentioned a number of sizing properties of the calcu-
lus: in particular that coercion terms preserve size, and that terms
and expressions are always of unit size (so that they can be kept in
registers).
These properties can be formalized as follows.
Theorem 2 (Size)
1. If #
2. If # then #i such that
3. If W # crc
4. If # val
5. If G;W # trm
6. If G;W # exp
7. If # w
PROOF. For each clause we proceed separately by induction on
typing derivations.
5 Representing the lambda calculus
One of the intended uses of l ord is as a target language for translation
from higher-level languages. To show how this can be done, and to
provide some intuition into how the language is used, we present
in this section a translation from the simply typed lambda calculus
with products and unit into the orderly lambda calculus.
We begin by defining a translation ptq that maps each ordinary
lambda calculus type to a l ord type.
The product case is unsurprising: we represent a pair as a pointer
to a heap-allocated record containing the sub-components. As discussed
in section 2, other representations are possible.
We represent the ordinary lambda calculus unit as a pointer to the
orderly lambda calculus unit. Recall that l ord . This means
that our chosen representation of unit is as a pointer to a zero-word
object. This corresponds precisely to the standard implementation
of values of type unit as a distinguished pointer to nothing (e.g. the
null pointer).
An analogous translation is defined at the term level. The interesting
case is the translation of pairing, since pairs are the only terms
requiring allocation. We begin by defining a l ord function pair.
reserve 2 as a (1)
in leta 1 .a
in leta 2 .a
in
in a 1 := x 1 as a # 1 (5)
in a 2 := x 2 as a # 2 (6)
in alloc(a # 1
in ret x (8)
The first line of the function reserves the space on the frontier from
which the pair will be created. This binds a single ordered variable
a which points to the beginning of this space. Line 2 gives the
names a 1 and a 2# respectively to the first and second words of the
newly allocated space. From the typing rule for reserve we can
see that the second location has an extra zero-byte value of type
unit attached, so lines 3 and 4 serve to split out and eliminate this.
Lines 5 and 6 initialize the two locations, renaming them to a # 1 and
a # 2 . Finally, line 7 allocates the initialized space into the heap and
names the result x, which becomes the return value of the function
in line 8.
This definition demonstrates how the various operations interact to
permit low-level code to be written in a relatively high-level man-
ner. In particular, there is no mention of offsets at all: everything
is done in terms of standard alpha-varying variables. It may seem
that this code is somewhat verbose, but it is simple to define syntactic
abbreviations and composite terms that eliminate much of the
verbosity. For example, in the common case for initialization terms
where the coercion term Q is a variable, we may take advantage of
alpha-conversion to simply re-use the old variable name, yielding a
more standard looking assignment syntax.
It is also trivial to define a composite reserve operation that pre-computes
the offset variables.
Working out the definition of this term is left as an exercise to the
reader, but using these abbreviations, we can write the pair constructor
quite succinctly.
reserve
in a 1 := x 1
in a 2 := x 2
in alloc(a 1
in ret x
The elimination forms for pairs can be given succinct definitions
using the direct load defined in Figure 6.
fst
load
in ret x 1
load
in ret x 2
The remainder of the translation of the simply typed lambda calculus
is straightforward. All variables introduced by the translation
are assumed to be fresh.
pl(x:t).eq
pe
in let x
in x 1 x 2
in let x
in let x
in let
in ret x
in fst x
in snd x
5.1 Coalescing reservation
Translating simply typed lambda calculus terms into the orderly
lambda calculus breaks the high level memory abstractions and exposes
a finer grain of detail. Exposing these details can enable optimizations
not expressible at the more abstract level. A simple example
of this is the ability to coalesce multiple calls to the allocator.
For example, consider the result of translating the term (3,(4,5))
under the above translation (with some minor simplifications).
in a 1 := 4as a # 1
in a 2 := 5as a # 2
in alloc(a # 1 .a # 2 ) as x
in ret x
in reserve 2 as[a 3 , a 4
in a 3 := 3as a # 3
in a 4 := x t as a # 4
in alloc(a # 3 .a # 4 ) as x
in ret x
This code fragment makes two separate calls to the allocator, each
reserving two words of space. It is easy to see that the second reserve
operation can be coalesced with the first, reducing the total
number of calls to the allocator.
opt
reserve 4 as[a 1 , a 2 , a 3 , a 4
in a 1 := 4as a # 1
in a 2 := 5as a # 2
in alloc(a # 1
in a 3 := 3as a # 3
in a 4 := x t as a # 4
in alloc(a # 3 .a # 4 ) as x
in ret x
This kind of optimization is commonly done in untyped compilers,
but here we can easily express it in a typed setting.
A further step to consider is to try to coalesce the two allocation op-
erations, in addition to coalescing the reservations. Unfortunately,
this is not in general possible in our setting. The problem is that
we currently cannot express pointers into the frontier-such pointers
would be difficult to typecheck since the types of locations in
the frontier can change. Therefore we are unable to initialize the
second field of the top level pair until we have moved the other pair
into the heap.
6 Extensions and future work
This paper has given a detailed presentation of the core of the orderly
lambda calculus, developing a high-level framework for discussing
issues of allocation and data-layout. The full language includes
an account of sums and recursive types that permits sum allocation
and tagging to be done using only the memory mechanisms
already described. In addition, we have extended the coercion level
to include ordered functions and application forms and shown that
a rich language of coercions is definable in this setting. Finally, we
have shown how the reserve, alloc, and write primitives can
be replaced by typed constants, eliminating the need to incorporate
special memory-management primitives into the language. The full
language is described in a separate technical report [13].
The most important question that we have not yet addressed is how
to give an account of the allocation of objects with dynamic extent.
The system we have developed so far is predicated on the ability to
statically predict the size of an object based on its type. For objects
such as arrays however, this is clearly not true.
While an ad-hoc treatment of arrays can be fairly easily integrated
into the language, this is unsatisfactory since the intention is to
make all allocation explicit through the same mechanism. A more
interesting possibility is to use a dependent type formalism [23] or a
type analysis formalism [4] to introduce a notion of dynamic extent
into the type system. We intend to explore this avenue further in the
future.
Another important area for future research is to attempt to account
for pointers into the frontier itself. As we saw in Section 5 we are
forced to allocate an object into the heap before we can initialize
other objects with a pointer to it, which prevents some useful optimizations
such as the destination passing style optimization [8].
7 Related work
Ordered logic and ordered type theory have been explored extensively
by Pfenning and Polakow [16, 15].
There is a significant amount of previous work applying ordinary
linear type theory to memory management [1, 22, 5, 7], but none
of it addresses (nor is intended to address) the question of separating
out allocation and initialization, and of giving a foundational
account of data layout.
The work that most closely addresses the issues that we discuss here
is the alias type formalism of Smith, Walker, and Morrisett [20]).
Alias types allow aliasing information to be tracked exactly in the
type system. A quasi-linear type system allows memory locations
to be destructively updated. Since aliasing is tracked exactly, an explicit
"free" operation is provided which de-allocates space. Some
very useful optimizations such as the destination passing style optimization
can be encoded fairly easily in this language. The alias
type formalism does not seem to provide for the explicit coalescing
of allocator calls, nor does it provide an explicit type theory for
describing data layout in the manner that we have attempted to do.



--R

Reference counting as a computational interpretation of linear logic.
A certifying compiler for Java.
Type structure for low-level programming langauges
Flexible type analysis.
Garbage collection based on a linear type system
A safe dialect of c

A functional represention of data structures with a hole.
A realistic typed assembly language.
Semantics of memory management for polymorphic languages.
From System F to typed assembly language.
The design and implementation of a certifying compiler.
Frank Pfen- ning
A judgmental reconstruction of modal logic.
Ordered linear logic and applications.
Natural deduction for intuitionistic non-commutative linear logic
Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic
Properties of terms in continuation-passing style in an ordered logical framework
An overview of the FLINT/ML compiler.
Alias types.

Operational interpretations of linear logic.
Eliminating array bound checking through dependent types.
--TR
A functional representation of data structures with a hole
Eliminating array bound checking through dependent types
The design and implementation of a certifying compiler
Quasi-linear types
Semantics of memory management for polymorphic languages
Flexible type analysis
Operational interpretations of linear logic
From system F to typed assembly language
A certifying compiler for Java
Type Structure for Low-Level Programming Languages
Natural Deduction for Intuitionistic Non-communicative Linear Logic
Ordered linear logic and applications

--CTR
Byoungro So , Mary W. Hall , Heidi E. Ziegler, Custom Data Layout for Memory Parallelism, Proceedings of the international symposium on Code generation and optimization: feedback-directed and runtime optimization, p.291, March 20-24, 2004, Palo Alto, California
Lars Birkedal , Noah Torp-Smith , John C. Reynolds, Local reasoning about a copying garbage collector, ACM SIGPLAN Notices, v.39 n.1, p.220-231, January 2004
Amal Ahmed , David Walker, The logical approach to stack typing, ACM SIGPLAN Notices, v.38 n.3, March
memory management;type theory;data representation;ordered logic