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 cal- culi. 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.
The Concurrent Calculi Formalisation Benchmark / M. Carbone, D. Castro-Perez, F. Ferreira, L. Gheri, F. Krogsdal Jacobsen, A. Momigliano, L. Padovani, A. Scalas, D. Tirore, M. Vassor, N. Yoshida, D. Zackon (LECTURE NOTES IN COMPUTER SCIENCE). - In: Coordination Models and Languages / [a cura di] I. Castellani, F. Tiezzi. - [s.l] : Springer, 2024 Jun 14. - ISBN 9783031626968. - pp. 149-158 (( convegno 26th IFIP WG 6.1 International Conference, COORDINATION 2024, Held as Part of the 19th International Federated Conference on Distributed Computing Techniques, DisCoTec 2024 tenutosi a Groningen nel 2024.
The Concurrent Calculi Formalisation Benchmark
A. Momigliano;
2024
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 cal- culi. 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.File | Dimensione | Formato | |
---|---|---|---|
cbench-2.pdf
accesso riservato
Tipologia:
Pre-print (manoscritto inviato all'editore)
Dimensione
297.08 kB
Formato
Adobe PDF
|
297.08 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
978-3-031-62697-5_9.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
254.57 kB
Formato
Adobe PDF
|
254.57 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.