Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Publication
Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Capture calculus is an extension of System Fsub 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, the latest version, namely the box calculus, 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.
Tiago André Pratas Borges, Anja Fröhlich, Estelle Lépine, Vanessa Pointet