The Concurrent Calculi Formalisation Benchmark
The POPLMark challenge sparked a flurry of work on machine-checked proofs. However, POPLMark (and its follow-up POPLMark Reloaded) were explicitly limited in scope, with benchmark problems that do not address concurrency. For this reason, we propose a new collection of benchmark problems with a focus on the issues encountered when mechanising message-passing concurrency using process calculi. Our benchmark problems concern linear handling of environments, scope extrusion, and coinductive reasoning. Our goal is to clarify, compare and advance the state of the art.
Sun 22 OctDisplayed time zone: Lisbon change
09:00 - 10:30
|A silent semantics for isorecursive session types
|Mechanising Multiparty Session Types: A Sound and Complete Projection
|The Concurrent Calculi Formalisation Benchmark
Marco Carbone IT University of Copenhagen, David Castro-Perez University of Kent, Francisco Ferreira Royal Holloway, University of London, Lorenzo Gheri University of Liverpool, Frederik Krogsdal Jacobsen Technical University of Denmark, Alberto Momigliano Università degli Studi di Milano, Luca Padovani University of Camerino, Alceste Scalas DTU, Martin Vassor University of Oxford, UK, Nobuko Yoshida University of Oxford