A Formalization of the Reversible Concurrent Calculus CCSKP in Beluga

TL;DR

This paper formalizes the reversible concurrent calculus CCSKP in the Beluga proof assistant, providing a machine-checked foundation for reasoning about reversible concurrent systems and their properties.

Contribution

It is the first formalization of CCSKP in a proof assistant, covering syntax, semantics, and advanced relations like dependence, independence, and connectivity.

Findings

First machine-checked formalization of CCSKP in Beluga

Explicit encoding of causality and concurrency relations

Revealed subtle details in formal proofs

Abstract

Reversible concurrent calculi are abstract models for concurrent systems in which any action can potentially be undone. Over the last few decades, different formalisms have been developed and their mathematical properties have been explored; however, none have been machine-checked within a proof assistant. This paper presents the first Beluga formalization of the Calculus of Communicating Systems with Keys and Proof labels (CCSKP), a reversible extension of CCS. Beyond the syntax and semantics of the calculus, the encoding covers state-of-the-art results regarding three relations over proof labels -- namely, dependence, independence and connectivity -- which offer new insights into the notions of causality and concurrency of events. As is often the case with formalizations, our encoding introduces adjustments to the informal proof and makes explicit details which were previously only sketched, some of which reveal to be less straightforward than initially assumed. We believe this work lays the foundations for future reversible concurrent calculi formalizations.