A Concurrent Pattern Calculus
并发模式演算（CPC）通过比较数据结构来驱动进程之间的交互，就像顺序模式演算驱动计算一样。通过从模式匹配推广到模式统一，交互变得对称，信息在两个方向上流动。CPC提供了一种自然语言来表达交易，其中信息交换是交互的关键。这种统一性使得某些模式比其他模式更具区分性;因此，行为理论必须考虑到这一点，这样互模拟就变得受制于模式的兼容性。许多流行的进程演算可以用CPC编码;这允许通过编码形式化的表达能力。
2014-08-20 cs.FL cs.LO
A Formalization of the Reversible Concurrent Calculus CCSKP in Beluga
本文首次在 Beluga 证明助手中形式化可逆并发演算 CCSKP，涵盖语法、语义及证明标签的依赖、独立和连通性关系，为可逆并发演算的机器验证奠定基础。
2025-08-19 cs.LO
Stubborn Transaction Reduction (with Proofs)
并行交织的指数级增长仍然是并发程序模型检验的一个基本挑战。偏序约简（POR）和事务约简（TR）都能减少并发系统中的交织次数。与POR不同，事务还减少了中间状态的数量。另一方面，现代POR技术提供了更动态的识别交换行为的方法，这是获得良好约简的关键任务。我们表明，交易减少可以使用相同的动态交换性，发现在顽固集POR。我们还比较了减少POR和TR，证明与几个例子，这些技术相辅相成。通过在模型检测器LTSmin中实现动态事务，我们将其有效性与原始静态TR和两种POR方法进行了比较。一些输入，包括现实的案例研究，表明新的动态TR可以在实践中超过POR。
2018-02-08 cs.LO
Probabilistic Rely-guarantee Calculus
Jones的可靠保证演算共享变量并发扩展到包括概率行为。我们使用的代数方法，结合和适应概率Kleene代数并发Kleene代数。稳健的代数相对于一般的概率事件结构语义。本文的主要贡献是建立在语义之上的可靠保证规则的集合。特别是，我们展示了如何获得的概率范围内的真实并发指称语义的可靠保证规则。这些规则的使用说明了一个简单的概率并发程序的详细验证：一个错误的Eratosthenes筛。
2015-06-02 cs.LO
Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars
并发程序设计语言的比较和并发环境下程序转换的正确性是本文研究的重点。作为标准，我们使用的上下文语义适应并发，在那里可能-以及应该-收敛观察。本文研究了并发Haskell（CH）核心语言与同步π演算的关系。上下文语义一方面对操作语义的细节给予宽容，另一方面对翻译后过程之间的相互作用提出了强烈的要求。我们的结果是，CH包含同步π演算。我们的主要任务是通过CH的并发原语（MVars）来发现和证明π演算通道编码的正确性。它们的行为类似于（阻塞）1位缓冲区，对共享内存进行建模。第一个开发的翻译使用一个额外的私人MVar的每一个通信。我们还自动生成和检查潜在的正确的翻译，重用MVar，其中一个MVar包含的消息和两个额外的MVar同步用于模拟一个通道的同步通信的pi演算。我们的自动实验结果导致推测，一个额外的MVar是不够的。
2020-08-31 cs.LO cs.PL
Truly Concurrent Pi-Calculi with Reversibility, Probabilism and Guards
著名的进程代数，如CCS，ACP和$π$ -演算，捕获基于双相似语义的交错并发。我们对CTC、APTC和$π_{tc}$等真并发进程代数做了一些工作，基于真并发双相似性，如pomset双相似性、step双相似性、history-preserving（hp-）双相似性和hereditary history-preserving（hhp-）双相似性来刻画真并发进程代数的并发性。真并发进程代数是相应的传统进程代数的推广。在本书中，我们将可逆性、概率论和保护引入真正的并发演算$π_{tc}$。
2021-08-24 cs.LO
Truly Concurrent Calculi with Reversibility, Probabilism and Guards
著名的进程代数，如CCS，ACP和$π$ -演算，捕获基于双相似语义的交错并发。我们对CTC、APTC和$π_{tc}$等真并发进程代数做了一些工作，基于真并发双相似性，如pomset双相似性、step双相似性、history-preserving（hp-）双相似性和hereditary history-preserving（hhp-）双相似性来刻画真并发进程代数的并发性。真并发进程代数是相应的传统进程代数的推广。在这本书中，我们将可逆性，概率论和警卫引入真正的并发演算CTC。
2021-08-15 cs.LO
Asynchronous Functional Sessions: Cyclic and Concurrent (Extended Version)
我们提出了并发GV（CGV），一个函数演算与消息传递的并发会话类型。相对于以前的演算，CGV增加了对并发计算和循环网络拓扑的支持。CGV的设计借鉴了APCP，一个会话类型的异步π演算在以前的工作。技术贡献是（i）CGV的语法，语义和类型系统;（ii）CGV到APCP的正确翻译;（iii）通过诉诸APCP的基于优先级的类型系统，建立无死锁CGV程序的技术。
2022-09-19 cs.LO
Asynchronous Functional Sessions: Cyclic and Concurrent
我们提出了并发GV（CGV），一个函数演算与消息传递的并发会话类型。相对于以前的演算，CGV增加了对并发计算和循环网络拓扑的支持。CGV的设计借鉴了APCP，一个会话类型的异步π演算在以前的工作。技术贡献是（i）CGV的语法，语义和类型系统;（ii）CGV到APCP的正确翻译;（iii）通过诉诸APCP的基于优先级的类型系统，建立无死锁CGV程序的技术。
2022-09-06 cs.LO
Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
本文提出Eiger-PORT+并发控制协议，实现强因果一致性TCCv，证明其性能最优读事务，驳斥开放猜想，并首次演绎验证复杂协议，性能优于现有方法。
2025-01-23 cs.DB cs.DC cs.FL
Proof-relevant $π$-calculus: a constructive account of concurrency and causality
我们提出了一个形式化的Agda理论的并发转换，残留，和因果等价的痕迹的π演算。我们的形式化采用德Bruijn指数和依赖类型的语法，并对齐的“证明转换”提出的Boudol和Castellani在CCS的上下文中与自然存在的Agda的表示标记的过渡关系的证明条款。我们的主要贡献是证明的“钻石引理”的残差的并发过渡和一个正式的定义等价的轨迹置换的过渡。在π演算中，转换表示当它们的动作涉及绑定名称时的传播绑定。为了适应这些情况下，我们需要一个更一般的钻石引理的目标状态的等价迹不再相同，但相关的编织重新布线绑定和自由的名称，以反映特定的交织的事件，涉及粘合剂。我们的方法可能是有用的建模并发在其他语言中的过渡进行元数据敏感的特定交织，如动态分配的内存地址。
2017-02-05 cs.DC cs.LO
A Coinductive Calculus for Asynchronous Side-effecting Processes
我们提出了一个抽象的并发进程的框架，其中原子步骤具有通用的副作用，处理效果的一元封装的原则。在这个框架中的过程是潜在的无限的选择，使用一元基上的最终余代数建模。作为这样的过程的演算，我们引入了并发扩展的莫吉的一元语言的影响。我们建立健全性和完整性的一个自然的方程式公理化的这种演算。此外，我们确定了一个corecursion计划，是明确定义的基础语言，并提供了灵活的表达手段的定义新的运营商的进程，如并行组合。作为一个工作的例子，我们证明了一个通用的互斥方案使用的验证逻辑建立在上面的方程演算的安全性。
2011-04-14 cs.LO
Reducing Opacity to Linearizability: A Sound and Complete Method
事务内存是一种代表程序员管理线程同步的机制，以便代码块以原子性的假象执行。事务内存的主要安全标准是不透明性，它定义了串行化并发事务的条件。证明不透明性是复杂的，因为它允许并发事务观察不同的内存状态，而TM实现通常基于一个共享存储。本文提出了一个健全的和完整的方法，基于粗粒度的抽象，减少证明的不透明性相对简单的正确性条件：线性化。我们使用我们的方法来验证TML和NORec从文献中，并显示我们的技术扩展到宽松的内存模型，表明这两个TSO下是不透明的，而不需要额外的围栏。我们的方法还阐明了TM设计在更高的抽象层次，作为一个应用程序，我们开发了一个变化的NORec与快速路径读取事务。我们所有的证明都是机械化的，无论是在Isabelle定理证明器还是PAT模型检查器中。
2016-10-04 cs.DC cs.DS cs.LO
An Operational Petri Net Semantics for the Join-Calculus
我们提出了一个并发操作Petri网语义的连接演算，指定并发和分布式系统的进程演算。在系统规范和实际实现之间经常存在差距，这是由规范方面的同步假设和实现中的异步交互组件造成的。联合演算是有希望的，以减少这一差距，提供一个抽象的规约语言，这是异步分布。经典的过程语义通过交错的方式建立了一个实际上独立的动作的隐式顺序。连接演算的语义也是如此。为了捕获这样的独立动作，基于步骤的语义，例如，如在Petri网上定义的。我们的Petri网语义的连接演算诱导步骤的行为在一个自然的方式。我们证明我们的语义行为等价于原来的连接演算语义的互模拟。我们将讨论如何加入特定的假设影响现有的概念，基于Petri网的可分布性。
2012-08-14 cs.LO
Concurrent Realizability on Conjunctive Structures
本文的重点是利用证明论和可实现性技术来探索并发计算的公理化。为了解决这个问题，我们重新定义的并发可实现性Beffara作为实现者的$π$ -演算与全球融合。我们定义一个变种的合取结构的RumeMiquey作为一个一般的结构，属于实现者和真值的可实现性。在安全可实现性方面，我们遵循Honda & Yoshida的工作，通过组合表示将实现子编码到代数结构中。在这第一项工作中，我们限制工作与$π$ -演算没有复制和其相应的类型系统是乘法线性逻辑（MLL）。
2021-12-29 cs.LO math.LO
Enabling Replications and Contexts in Reversible Concurrent Calculus
现有的形式主义的代数规范和表示网络的可逆代理遭受一些缺点。尽管多次尝试，通信系统演算（CCS）的可逆变格并没有提供令人满意的适应的概念，通常在“向前”的过程代数，如复制或上下文。它们似乎也未能利用源于可逆性的可能的新功能，例如基于它们如何复制允许反向计算的内存机制来区分多个复制的能力。现有的形式主义不允许在也有过去的上下文中执行过程的“热插拔”。最后，它们假设存在“永远新鲜”的键或标识符，如果实现得不好，可能会导致不必要的瓶颈和涉及所有线程的查找。在本文中，我们开始调查这些问题，首先设计了一个进程代数赋予的机制来生成标识符，而不需要咨询其他线程。我们使用这种演算来重铸CCS中的非确定性的可能表示，并作为副产品建立一个简单而直接的并发定义。我们的可逆演算，然后证明满足预期的属性，并允许精确地布局不同的表示复制的过程与内存。我们还观察到，迄今为止定义的可逆互模拟都不是我们的“可逆”上下文概念下的同余。
2021-03-29 cs.LO math.LO
Barbed Similarity for the $π$-Calculus in Beluga: A Case Study in Coinductive Reasoning
Università degli Studi di Milano（米兰大学）；Augusta University（奥古斯塔大学）
该研究在Beluga证明助手里形式化π演算的强带刺相似性，通过扩展先前工作纳入复制，基于刺和内部动作给出行为等价的共归纳编码，利用Beluga的共归纳得到简洁证明，证明了结合相关方法机械化并发演算的有效性。
2026-07-15 cs.LO
A Cut-Free Sequent Calculus for the Analysis of Finite-Trace Properties in Concurrent Systems
本文提出了一种无切割的序数演算LMC，用于分析并发系统中有限迹性质，通过闭包ℓ-单形的代数抽象实现逻辑系统的正确性和完备性。
2025-12-05 cs.LO math.LO
Games, mobile processes, and functionss -- alternating, concurrent, and well-bracketed semantics
Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004（南特大学，中央理工学院南特分校，法国国家信息与自动化研究所，LS2N实验室）
本文建立λ演算的π演算编码与操作博弈语义的紧密联系，推导其等价关系一致性，实现结果与技术双向转移，得到新行为等价关系及完全抽象结果，并针对按值调用与按名调用展开说明。
2026-10-07 cs.LO
Typed Non-determinism in Concurrent Calculi: The Eager Way
本文提出一种基于急切语义的会话类型π-演算，以处理非确定性与线性性的张力，确保无死锁性，并通过翻译资源λ-演算展示其表达能力。
2024-12-07 cs.LO cs.PL
A Beluga Formalization of the Harmony Lemma in the $π$-Calculus
针对π演算和谐引理缺乏严格证明的问题，研究者在Beluga中实现了该引理在基准测试π演算子片段上的形式化，借鉴HOAS方法并提出两种实用编码技术，为并发演算形式化基准提供贡献。
2024-07-09 cs.LO
Checking Robustness Between Weak Transactional Consistency Models
对数据库的并发访问通常封装在事务中，以便能够与其他并发计算隔离并对故障具有弹性。现代数据库为事务提供了各种语义，对应于一致性和可用性之间的不同权衡。由于较弱的一致性模型提供更好的性能，因此一个重要的问题是调查给定程序所需的最弱一致性级别（以满足其规范）。作为处理这个问题的一种方式，我们调查的问题，检查是否一个给定的程序具有相同的一组行为时，更换一个较弱的一致性模型。这种被称为鲁棒性的特性通常意味着在削弱一致性时保留程序的任何规范。我们专注于一致性模型的鲁棒性问题，这是弱于标准的串行化，即因果一致性，前缀一致性，快照隔离。我们发现，检查这些模型之间的鲁棒性是多项式时间减少到一个状态可达性问题下的串行化。我们使用这种减少也得到一个务实的证明技术的基础上，利普顿的减少理论，允许证明程序的鲁棒性。我们已经将我们的技术应用于几个具有挑战性的应用程序，从分布式系统和数据库的文献。
2021-01-22 cs.LO cs.PL
Static Application-Level Race Detection in STM Haskell using Contracts
编写并发程序是一项艰巨的任务，即使使用高级同步原语（如事务存储器）和具有良好控制副作用的函数式语言（如Haskell），因为进程之间产生的干扰可能发生在不同的级别，并且以非常微妙的方式发生。当线程将共享数据保留或公开为与应用程序逻辑或数据的真实含义不一致的状态时，就会出现问题。在本文中，我们建议将合同与交易相关联，并定义了一个程序转换，使得在STM Haskell的上下文中扩展静态合同检查成为可能。因此，我们能够静态地检查STM Haskell程序的每个事务处理共享数据的方式，即以用户定义的布尔函数的形式表示的给定一致性属性被保留。这确保了在并发程序的执行过程中不会发生不良干扰。
2013-12-10 cs.DC cs.LO cs.PL
Truly Concurrent Process Algebra with Localities
著名的进程代数，如CCS，ACP和$π$ -演算，捕获基于双相似语义的交错并发。我们对CTC、APTC和$π_{tc}$等真并发进程代数做了一些工作，基于真并发双相似性，如pomset双相似性、step双相似性、history-preserving（hp-）双相似性和hereditary history-preserving（hhp-）双相似性来刻画真并发进程代数的并发性。真并发进程代数是相应的传统进程代数的推广。在这本书中，我们引入地方到真正的并发进程代数，工作的基础上进程代数与地方。
2021-09-10 cs.LO
Reversible Quantum Process Algebra
真并发进程代数是传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数的推广。在可逆进程代数和概率真并发进程代数方面也做了一些工作。在本书中，我们利用可逆的真正并发进程代数APRTC和APPTC来建模量子计算，并统一量子和经典计算。
2021-08-05 cs.LO
Truly Concurrent Process Algebra to Unifying Quantum and Classical Computing
真并发进程代数是传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数的推广。现在，是时候利用真正的并发进程代数APTC和APPTC来建模量子计算并统一量子计算和经典计算了。在这本书中，我们介绍了APTC的原理，利用APTC统一量子和经典计算及其在量子通信协议验证中的应用，利用APPTC统一量子和经典计算及其在量子通信协议验证中的应用。
2021-10-25 cs.LO
Processes, Systems and Tests: Defining Contextual Equivalences
在这份立场文件中，我们想提供并捍卫一个新的模板来研究程序之间的等价性--在并发计算的进程代数的特定框架中。我们相信，我们的分层开发模型将澄清程序员和测试人员的任务和职责之间的区别。它也将启发已经运行在不同的进程代数，如通信系统的演算，$π$演算-也在其分布式版本-或移动ambients.我们的区别开始细分的概念过程本身在三个概念上分离的实体，我们称之为\emph{Processes}，\emph{Systems}和\emph{Tests}。虽然可以观察到的作用和同余定义中的微妙之处已经被深入研究，但\emph{not every process can be tested}和\emph{the tester should have access to a different set of tools than the programmer}奇怪地被排除在外，或者至少不经常正式讨论。我们认为，这个盲点来自于对上下文的不充分规范--进行比较的环境--我们用一个简单的Java例子来说明我们的声明，\enquote{stay the same}并发语言，但也用$λ$ -演算和并发语言的现有实现来支持它。
2021-10-05 cs.DC cs.FL cs.LO
Reversible Quantum Process Algebra with Guards
真并发进程代数是传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数的推广。在可逆进程代数和概率真并发进程代数方面也做了一些工作。在这本书中，我们利用可逆的真正并发进程代数APRTC和概率进程代数APPTC来建模量子计算，并统一量子和经典计算。
2021-08-05 cs.LO
Security Analyses of Quantum Communication Protocols
真并发进程代数是对传统的真并发进程代数、CTC到CCS、APTC到ACP、$π_{tc}$到$π$演算、APPTC到概率进程代数的推广。在本书中，我们利用真并发进程代数APTC和APPTC来建模量子计算，并统一量子计算和经典计算。
2021-07-28 cs.LO
Towards Proving Liveness on Weak Memory (Extended Version)
本文提出了一种基于弱公平性的证明演算，用于在弱内存模型中证明活锁性，并应用于票锁算法以证明其在多种内存模型下的无饥饿性。
2026-02-23 cs.LO
Probabilistic Process Algebra for True Concurrency
著名的进程代数，如CCS，ACP和$π$ -演算，捕获基于双相似语义的交错并发。我们对CTC、APTC和$π_{tc}$等真并发进程代数做了一些工作，基于真并发双相似性，如pomset双相似性、step双相似性、history-preserving（hp-）双相似性和hereditary history-preserving（hhp-）双相似性来刻画真并发进程代数的并发性。真并发进程代数是相应的传统进程代数的推广。在这本书中，我们引入概率到真正的并发进程代数，基于概率进程代数的工作。
2021-07-28 cs.LO
Mapping Fusion and Synchronized Hyperedge Replacement into Logic Programming
在本文中，我们比较了三种不同的形式主义，可用于该地区的模型，分布式，并发和移动系统。特别是，我们分析了进程演算，融合演算，图形变换中的同步超边替换与霍尔同步（HSHR）的方法和逻辑编程之间的关系。我们提出了一个翻译融合演算到HSHR（而融合演算使用米尔纳同步），并证明了融合演算和HSHR转换的减少语义之间的对应关系。我们还提出了一个映射从HSHR到一个事务版本的逻辑编程，并证明有一个完整的对应关系之间的两个形式主义。从融合演算到逻辑编程的映射是有趣的，因为它显示了两种形式主义之间的紧密类比，特别是在处理名称生成和移动性方面。根据HSHR的中间步骤是方便的，因为图转换允许多个远程同步，如Fusion Calculus语义所要求的。
2006-01-15 cs.LO cs.PL
