SPLASH 2023 (series) / ST30 (series) / 30 Years of Session Types /
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
Sun 22 Oct
Displayed time zone: Lisbon change
09:00 - 10:30 | |||
09:00 30mTalk | A silent semantics for isorecursive session types ST30 Janek Spaderna University of Freiburg, Germany, Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos LASIGE, University of Lisbon | ||
09:30 30mTalk | Mechanising Multiparty Session Types: A Sound and Complete Projection ST30 Marco Carbone IT University of Copenhagen, Dawit Tirore IT University of Copenhagen, Denmark, Jesper Bengtson IT University of Copenhagen, Denmark | ||
10:00 30mTalk | The Concurrent Calculi Formalisation Benchmark ST30 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 | ||