数据布局的类型论视角
Data Layout from a Type-Theoretic Perspective
AI总结：
本文提出一种基于直觉主义逻辑半公理相继式演算的类型论数据布局方法，通过细化地址结构支持替代布局，并添加递归类型，可作为编译器中间语言或增强程序员控制。
摘要：
数据布局的具体细节对于函数式程序的效率以及与外部库的交互可能至关重要。在本文中，我们发展了一种数据布局的类型论方法，该方法可用作编译器中的类型化中间语言，或为程序员提供更多控制。我们的出发点是直觉主义逻辑的半公理相继式演算的计算解释，该解释定义了单元格和地址的抽象概念。我们细化了这一语义，使地址具有更多结构以反映可能的替代布局，而无需从根本上偏离直觉主义逻辑。随后，我们添加递归类型，并探索所得语言的示例程序和性质。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
