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.

翻译：可逆并发演算是一类并发系统的抽象模型，其中任何动作都潜在地可被撤销。在过去的几十年里，不同的形式化方法被提出，其数学性质也得到了探索；然而，尚未有工作在证明辅助工具中进行过机器验证。本文首次在 Beluga 中对带密钥与证明标签的通信系统演算（CCSKP）进行了形式化，该演算是 CCS 的一个可逆扩展。除了演算的语法和语义，该编码还涵盖了关于证明标签之间三种关系（即依赖、独立与连通性）的最新研究成果，这些关系为事件间的因果性与并发性概念提供了新的见解。与形式化工作的常见情况类似，我们的编码对非形式化证明进行了调整，并明确了先前仅粗略描述的细节，其中一些细节被证明比最初设想的更为复杂。我们相信这项工作为未来可逆并发演算的形式化奠定了基础。