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.

翻译：数据布局的具体细节对于函数式程序的效率以及与外部库的交互至关重要。本文提出了一种基于类型理论的数据布局方法，可将其用作编译器中的带类型中间语言，或赋予程序员更强的控制能力。我们以直觉逻辑的半公理化相继式演算的计算解释为出发点，该演算定义了抽象的单元和地址概念。我们对这一语义进行精化，使地址具有更丰富的结构，以在不根本偏离直觉逻辑的前提下反映可能的替代布局方案。随后引入递归类型，并探讨了所得语言中的示例程序及其性质。