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_<:□), 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.
Tue 24 OctDisplayed time zone: Lisbon change
14:00 - 15:30
|A Mechanized Theory of the Box Calculus|
|Compositional Reasoning about Advanced Iterator Patterns in Rust|
Aurel Bílý ETH Zurich, Jonas Hansen ETH Zurich, Alexander J. Summers University of British Columbia, Peter Müller ETH ZurichFile Attached
|Oxidize: A Step-Debugger for Static Semantics|
Peter Chon Harvard University, Dimi Racordon Northeastern University, USA, Nada Amin Harvard UniversityFile Attached