The Concurrent Calculi Formalisation Benchmark

Proposal

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.

Paper about the benchmark

A paper describing the background and motivation for the benchmark was published in the proceedings of COORDINATION 2024. It can be found here.

Challenge Descriptions

The detailed descriptions of the challenges can be found here.

Solutions

Authors Challenge Proof assistant Technique Links
Gabriele Cecilia and Alberto Momigliano Scope extrusion Beluga weak HOAS Code, Paper
Marco Carbone Linearity + Scope extrusion Coq Linearity predicates + de Bruijn indices To appear
Claudia Raffaelli and Luca Padovani Coinduction Agda Experimenting To appear
Daniel Zackon, Chuta Sano, Brigitte Pientka and Alberto Momigliano Linearity Beluga Explicit contexts with resource algebra, weak HOAS To appear
Chuta Sano, Daniel Zackon, Brigitte Pientka and Alberto Momigliano Linearity Beluga Linearity predicates, weak HOAS To appear

Inspiration

We have collected a list of existing mechanisations of concurrent calculi that might be serve as inspiration for your solution. See it here.

Who are we? (so far)

So far, the members are (in no particular order1):

Do you want to contact us and participate?

We use this this web group to communicate.