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.

翻译：数据布局的具体细节对函数式程序的效率及与外部库的交互至关重要。本文提出一种基于类型论的数据布局方法，可作为编译器中的带类型中间语言，或赋予程序员更精细的控制能力。我们的出发点是直觉逻辑半公理序列演算的计算解释，该解释定义了抽象意义上的单元与地址概念。我们对此语义进行精化，使地址具备更多结构以反映可能的备选布局，同时不从根本上偏离直觉逻辑。随后我们引入递归类型，并通过示例程序探索所得语言的性质。