Capture calculus has recently been proposed as a solution to effect checking, achieved by tracking the captured references of terms in the types. Boxes, along with the box and unbox operations, are a crucial construct in capture calculus, which maintains the hygiene of types and improves the expressiveness of polymorphism over capturing types. Despite their usefulness in the formalism, boxes would soon become a heavy notational burden for users when the program grows. It thus necessitates the inference of boxes when integrating capture checking into a mainstream programming language. In this paper, we develop a formalisation of box inference for capture calculus. We begin by introducing a semi-algorithmic variant of the capture calculus, from which we derive an inference system where typed transformations are applied to complete missing box operations in programs. Then, we propose a type-level system that performs provably equivalent inference on the type level, without actually transforming the program. In the metatheory, we establish the relationships between these systems and capture calculus, thereby proving both the soundness and the completeness of box inference.

翻译：捕获演算最近被提出作为一种效果检查的解决方案，通过在类型中追踪项所捕获的引用来实现这一目的。盒子（box）及其对应的装箱（box）和拆箱（unbox）操作是捕获演算中的关键构造，它们维护了类型的整洁性，并增强了针对捕获类型的多态表达能力。尽管盒子在形式化中非常有用，但随着程序规模的增长，它们很快会成为用户沉重的记法负担。因此，在将捕获检查集成到主流编程语言中时，对盒子进行推断是必要的。在本文中，我们为捕获演算开发了一种盒子推断的形式化方法。我们首先引入捕获演算的半算法变体，并由此推导出一个推断系统，在该系统中通过应用类型化变换来补全程序中缺失的盒子操作。然后，我们提出一个类型级系统，它可以在不实际转换程序的情况下，在类型层面执行可证明等价的推断。在元理论中，我们建立了这些系统与捕获演算之间的关系，从而证明了盒子推断的可靠性和完备性。