形式化捕获演算中的盒子推理
摘要：捕获演算最近被提出作为一种解决效果检查的方法，通过追踪类型中术语的捕获引用来实现。在捕获演算中，盒子与盒子和取出操作一起被构建为维护类型的卫生和提高捕获类型的多态性的关键。尽管盒子在形式化中很有用，但当程序变得庞大时，盒子很快就会成为用户的一个沉重符号负担。因此，在将捕获检查集成到主流编程语言中时，需要进行盒子的推断。在本文中，我们为捕获演算开发了盒子推断的形式化。我们首先介绍一种半算法变体的捕获演算，从中推导出一种推断系统，该系统在程序中应用类型变换以完成缺失的盒子操作。然后，我们提出了一种在类型层面上执行可证明等价推断的类型级系统，而无需实际转换程序。在元理论中，我们建立了这些系统与捕获演算之间的关系，从而证明了盒子推断的完备性和声音性。
作者：Yichen Xu and Martin Odersky
论文ID：2306.06496
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-13