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.

翻译：数据布局的具体特性对于功能程序的效率和与外部图书馆的互动可能很重要。 在本文中, 我们开发了一种类型理论方法, 用于数据布局, 可以在编译器中用作打字中间语言, 或者给予程序员更多的控制。 我们的出发点是对直觉逻辑的半轴序列积分进行计算解释, 以定义单元格和地址的抽象概念。 我们改进了这个语义, 使地址具有更多的结构, 以反映可能的替代布局, 而不会从根本上偏离直觉逻辑 。 然后我们添加递归类型, 并探索由此产生的语言的示例程序及属性 。