The Concurrent Calculi Formalisation Benchmark

Marco Carbone; David Castro-Perez; Francisco Ferreira; Lorenzo  Gheri; Frederik  Krogsdal Jacobsen; Alberto  Momigliano; Luca  Padovani; Alceste Scalas; Dawit Tirore; Martin  Vassor; Nobuko Yoshida; Daniel  Zackon

doi:10.1007/978-3-031-62697-5_9

The Concurrent Calculi Formalisation Benchmark

Marco Carbone, David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, Frederik Krogsdal Jacobsen, Alberto Momigliano, Luca Padovani, Alceste Scalas, Dawit Tirore, Martin Vassor, Nobuko Yoshida, Daniel Zackon

Department of Computer Science

Research output: Contribution to conference › Paper › peer-review

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.

Original language	English
Pages	149-158
DOIs	https://doi.org/10.1007/978-3-031-62697-5_9
Publication status	Published - 11 Jun 2024
Event	COORDINATION 2024 - 26th International Conference on Coordination Models and Languages - Groningen, Netherlands Duration: 18 Jun 2024 → 20 Jun 2024

Conference

Conference	COORDINATION 2024 - 26th International Conference on Coordination Models and Languages
Country/Territory	Netherlands
City	Groningen
Period	18/06/24 → 20/06/24

Access to Document

10.1007/978-3-031-62697-5_9

Embargoed Document

Accepted manuscript
Accepted author manuscript, 315 KB
Embargo ends: 11/06/25

Cite this

Carbone, M., Castro-Perez, D., Ferreira, F., Gheri, L., Krogsdal Jacobsen, F., Momigliano, A., Padovani, L., Scalas, A., Tirore, D., Vassor, M., Yoshida, N., & Zackon , D. (2024). The Concurrent Calculi Formalisation Benchmark. 149-158. Paper presented at COORDINATION 2024 - 26th International Conference on Coordination Models and Languages, Groningen, Netherlands. https://doi.org/10.1007/978-3-031-62697-5_9

@conference{0de55e1cbc1d4c8dac8ad5ba8dc3e8e6,

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.",

author = "Marco Carbone and David Castro-Perez and Francisco Ferreira and Lorenzo Gheri and {Krogsdal Jacobsen}, Frederik 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",

pages = "149--158",

note = "COORDINATION 2024 - 26th International Conference on Coordination Models and Languages ; Conference date: 18-06-2024 Through 20-06-2024",

}

Carbone, M, Castro-Perez, D, Ferreira, F, Gheri, L, Krogsdal Jacobsen, F, Momigliano, A, Padovani, L, Scalas, A, Tirore, D, Vassor, M, Yoshida, N & Zackon , D 2024, 'The Concurrent Calculi Formalisation Benchmark', Paper presented at COORDINATION 2024 - 26th International Conference on Coordination Models and Languages, Groningen, Netherlands, 18/06/24 - 20/06/24 pp. 149-158. https://doi.org/10.1007/978-3-031-62697-5_9

TY - CONF

T1 - The Concurrent Calculi Formalisation Benchmark

AU - Carbone, Marco

AU - Castro-Perez, David

AU - Ferreira, Francisco

AU - Gheri, Lorenzo

AU - Krogsdal Jacobsen, Frederik

AU - Momigliano, Alberto

AU - Padovani, Luca

AU - Scalas, Alceste

AU - Tirore, Dawit

AU - Vassor, Martin

AU - Yoshida, Nobuko

AU - Zackon , Daniel

PY - 2024/6/11

Y1 - 2024/6/11

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-031-62697-5_9

DO - 10.1007/978-3-031-62697-5_9

M3 - Paper

SP - 149

EP - 158

T2 - COORDINATION 2024 - 26th International Conference on Coordination Models and Languages

Y2 - 18 June 2024 through 20 June 2024

ER -