Ordered type theory is a natural 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 accounting 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.