A Mechanized Theory of the Box Calculus

TL;DR

This paper presents a complete mechanization of the box calculus, an extension of System F<: that manages variable capture and capabilities, using Coq to ensure soundness and correctness.

Contribution

It provides the first mechanized proof of the box calculus's theory, addressing previous gaps where only paper proofs existed.

Findings

Mechanization in Coq was successful and complete.

Insights into the design and metatheory of capture calculus.

Challenges encountered and overcome during formalization.

Abstract

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.