论文标题
从类型理论的角度来看数据布局
Data Layout from a Type-Theoretic Perspective
论文作者
论文摘要
数据布局的细节对于功能程序的效率和与外部库的互动可能很重要。在本文中，我们为数据布局开发了一种类型的理论方法，该方法可以用作编译器中的类型中间语言或为程序员提供更多的控制。我们的起点是对直觉逻辑的半轴序列序列的计算解释，该逻辑定义了细胞和地址的抽象概念。我们完善了这种语义，因此地址具有更多的结构，可以反映可能的替代布局，而不会从根本上偏离直觉逻辑。然后，我们添加递归类型，并探索所得语言的示例程序和属性。
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.
