CCSKP 可逆并发微积分Beluga 中的形式化

可逆并发微积分是用于建模并发系统的抽象模型，任何动作都可能被撤销。过去几十年间，已发展出不同的形式化并探讨其数学性质；然而，none被形式化地机器检查过。本文提出了CCSKP（Communicating Systems with Keys and Proof labels 的可逆扩展）在Beluga中的首个形式化。除了微积分的语法与语义，编码涵盖关于proof labels的三类关系的最新结果——即dependence、independence与connectivity——为理解事件的因果性与并发性提供了新见解。正如通常情况，我们的编码引入了对不严格的证明的调整，并明确了此前仅勾勒的细节，其中一些细节不如最初假设的那样简单。我们认为此工作为未来可逆并发微积分的形式化奠定了基础。