A Mechanized Theory of the Box Calculus
summary
Mechanization of the Box Calculus appears as a complete Coq development that formalizes System CC_<:□ with Coq mechanization and produces a verified soundness proof available on GitHub. It implements boxes/unbox to hide and reveal capture sets, enforces pure type-variable bounds, and uses monadic normal form plus locally nameless + cofinite quantification for binding. The mechanization merges pre-types and types into one inductive, simplifies well-formedness, and shrinks the proof from 12,000 → 7,000 lines, claiming the implementation works and is reusable.
AI-written summary · about