证明相关的$π$ -演算：并发性和因果关系的建设性说明
Proof-relevant $π$-calculus: a constructive account of concurrency and causality
摘要：
我们提出了一个形式化的Agda理论的并发转换，残留，和因果等价的痕迹的π演算。我们的形式化采用德Bruijn指数和依赖类型的语法，并对齐的“证明转换”提出的Boudol和Castellani在CCS的上下文中与自然存在的Agda的表示标记的过渡关系的证明条款。我们的主要贡献是证明的“钻石引理”的残差的并发过渡和一个正式的定义等价的轨迹置换的过渡。在π演算中，转换表示当它们的动作涉及绑定名称时的传播绑定。为了适应这些情况下，我们需要一个更一般的钻石引理的目标状态的等价迹不再相同，但相关的编织重新布线绑定和自由的名称，以反映特定的交织的事件，涉及粘合剂。我们的方法可能是有用的建模并发在其他语言中的过渡进行元数据敏感的特定交织，如动态分配的内存地址。
英文摘要：
We present a formalisation in Agda of the theory of concurrent transitions, residuation, and causal equivalence of traces for the pi-calculus. Our formalisation employs de Bruijn indices and dependently-typed syntax, and aligns the "proved transitions" proposed by Boudol and Castellani in the context of CCS with the proof terms naturally present in Agda's representation of the labelled transition relation. Our main contributions are proofs of the "diamond lemma" for the residuals of concurrent transitions and a formal definition of equivalence of traces up to permutation of transitions. In the pi-calculus transitions represent propagating binders whenever their actions involve bound names. To accommodate these cases, we require a more general diamond lemma where the target states of equivalent traces are no longer identical, but are related by a braiding that rewires the bound and free names to reflect the particular interleaving of events involving binders. Our approach may be useful for modelling concurrency in other languages where transitions carry metadata sensitive to particular interleavings, such as dynamically allocated memory addresses.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
