The capture calculus is an extension of System F<: that tracks free variables of terms in their type, allowing one to represent capabilities while limiting their scope. While previous calculi had mechanized soundness proofs -- notably System CF<: -- the latest version, namely the box calculus (System CC<:box), only had a paper proof. We present here our work on mechanizing the theory of the box calculus in Coq, and the challenges encountered along the way. While doing so, we motivate the current design of capture calculus, in particular the concept of boxes, from both user and metatheoretical standpoints. Our mechanization is complete and available on GitHub.

翻译：捕获演算是System F<:的一种扩展，它通过在类型中追踪项的自由变量，使得我们能够表示能力（capabilities）并限制其作用域。尽管先前的演算（特别是System CF<:）已具备机械化的可靠性证明，但最新版本——即盒式演算（System CC<:box）——此前仅有纸面证明。本文介绍了我们在Coq中实现盒式演算理论机械化的相关工作及过程中遇到的挑战。在此过程中，我们从用户和元理论的双重视角阐明了当前捕获演算的设计动机，特别是盒（boxes）这一概念。我们的机械化工作已全部完成，并可在GitHub上获取。