  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.
