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.

翻译：数据布局的具体细节对函数式程序的效率以及与外部库的交互至关重要。本文从类型论角度出发，提出一种可作用于数据布局的方法，该方法既能作为编译器中的带类型中间语言，也可赋予程序员更强的控制能力。我们的研究起点是对直觉逻辑半公理相继式演算的计算解释，该演算定义了细胞和地址的抽象概念。在此基础上，我们对这一语义进行精炼，使地址具备更丰富的结构以反映可能的替代布局方案，且不从根本上背离直觉逻辑。随后，我们引入递归类型，并通过示例程序及所得语言的性质展开探索。