@inbook{04acb22d625d4e9486f596d7ab4267fe,
title = "The Concurrent Calculi Formalisation Benchmark",
abstract = "POPLMark and POPLMark Reloaded sparked a flurry of work on machine-checked proofs, and fostered the adoption of proof mechanisation in programming language research. Both challenges were purposely limited in scope, and they do not address concurrency-related issues. We propose a new collection of benchmark challenges focused on the difficulties that typically arise when mechanising formal models of concurrent and distributed programming languages, such as process calculi. Our benchmark challenges address three key topics: linearity, scope extrusion, and coinductive reasoning. The goal of this new benchmark is to clarify, compare, and advance the state of the art, fostering the adoption of proof mechanisation in future research on concurrency.",
keywords = "Mechanisation, Process calculi, Benchmark, Linearity, Scope extrusion, Coinduction",
author = "Marco Carbone and David Castro-Perez and Francisco Ferreira and Lorenzo Gheri and Jacobsen, \{Frederik Krogsdal\} and Alberto Momigliano and Luca Padovani and Alceste Scalas and Dawit Tirore and Martin Vassor and Nobuko Yoshida and Daniel Zackon",
year = "2024",
month = jun,
day = "11",
doi = "10.1007/978-3-031-62697-5\_9",
language = "English",
isbn = "978-3-031-62696-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer Nature Switzerland",
pages = "149--158",
booktitle = "Coordination Models and Languages",
}