  The specifics of data layout can be important for the efficiency of
functional programs and interaction with external libraries. In this paper, we
develop a type-theoretic approach to data layout that could be used as a typed
intermediate language in a compiler or to give a programmer more control. Our
starting point is a computational interpretation of the semi-axiomatic sequent
calculus for intuitionistic logic that defines abstract notions of cells and
addresses. We refine this semantics so addresses have more structure to reflect
possible alternative layouts without fundamentally departing from
intuitionistic logic. We then add recursive types and explore example programs
and properties of the resulting language.
