Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
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