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 \emph{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.