Proceedings Fifth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software
PLACES 2012（全称：面向以并发和通信为中心的软件的程序设计语言方法）是PLACES研讨会系列的第五版。自2008年第一届PLACES加入DisCoTec之后，自2009年以来，该研讨会每年都是ETAPS的一部分，现在是ETAPS卫星活动的一部分。PLACES 2012于3月31日在爱沙尼亚塔林举行。开办这一系列讲习班是为了促进新的程序设计语言思想应用于为并行和通信是内在方面的系统开发软件这一日益重要的问题。这包括用于多核系统和大规模分布式和/或面向服务的系统的软件。PLACES的范围包括新的程序设计语言特性、全新的程序设计语言设计、新的类型系统、新的语义方法、新的程序分析技术和新的实现机制。今年的论文征集活动共收到17份论文，方案委员会从中挑选了10份论文在讲习班上介绍。讲习班结束后，所有作者都应邀编写了论文的修订本，以列入《欧洲条约汇编》的议事录。六篇论文的作者接受了邀请，这些论文构成了本卷。
2013-02-23 cs.DC cs.LO cs.PL
Translating between models of concurrency
Hoare的通信顺序过程（CSP）承认与van Glabbeek频谱密切相关的语义模型的丰富宇宙。在本文中，我们研究有限观测模型，其中至少有六个已确定的CSP，即痕迹，稳定故障，复活，接受，拒绝测试和有限的线性观测。我们将展示如何使用最近推出的\emph{priority}运营商转换到跟踪细化（语言包含）测试在这些模型中的细化问题。此外，我们能够将其推广到任何（理性的）有限观测模型。除了理论上的兴趣，这是具有实际意义的，因为国家的最先进的细化检查工具FDR4目前只支持两个这样的模型。特别是，我们研究如何有可能检查细化的离散版本的定时故障模型，支持定时CSP。
2019-04-22 cs.FL cs.LO
Proceedings Combined 21st International Workshop on Expressiveness in Concurrency and 11th Workshop on Structural Operational Semantics
本卷包含2014年9月1日在意大利罗马举行的第21届并发表达性国际研讨会和第11届结构操作语义研讨会（EXPRESS/SOS 2014）的会议记录，作为CONCUR 2014的附属研讨会，第25届并发理论国际会议。EXPRESS研讨会旨在汇集对各种形式系统和语义概念的表达感兴趣的研究人员，特别是在并发领域。传统上，他们的重点是比较编程概念（如并发、函数、命令、逻辑和面向对象编程）和计算的数学模型（如进程代数、Petri网、事件结构、模态逻辑和重写系统）之间的相对表达能力。自1994年以来，EXPRESS系列研讨会已经成功举办，多年来，这一重点已经得到广泛的理解。SOS研讨会的目的是成为一个论坛的研究人员，学生和从业人员感兴趣的新发展，未来的调查方向，在结构操作语义领域。SOS研讨会系列的具体目标之一是在从事SOS理论和实践工作的并发和程序设计语言社区之间建立协同作用。SOS在其他领域的应用报告也非常受欢迎，包括：生物系统的建模和分析，计算机系统编程的安全性，嵌入式系统的建模和分析，中间件和协调语言的规范，程序设计语言语义和实现，静态分析软件和硬件验证，以及特定领域语言和基于模型的工程的语义。
2014-08-06 cs.LO cs.PL
Proceedings Combined 20th International Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics
本卷包含2013年8月26日在阿根廷布宜诺斯艾利斯举行的第20届并发表达性国际研讨会和第10届结构操作语义研讨会（EXPRESS/SOS 2013）的会议记录，作为CONCUR 2013的附属研讨会，第24届并发理论国际会议。EXPRESS研讨会旨在汇集对各种形式系统和语义概念的表达感兴趣的研究人员，特别是在并发领域。传统上，他们的重点是编程概念（例如并发、函数式、命令式、逻辑和面向对象编程）之间的比较以及计算数学模型（例如进程代数、Petri网、事件结构、模态逻辑和重写系统）之间的比较。基于它们的相对表达能力。自1994年以来，EXPRESS系列研讨会已经成功举办，多年来，这一重点已经得到广泛的理解。SOS研讨会的目的是成为一个论坛的研究人员，学生和从业人员感兴趣的新发展，未来的调查方向，在结构操作语义领域。SOS研讨会系列的具体目标之一是在从事SOS理论和实践工作的并发和程序设计语言社区之间建立协同作用。SOS在其他领域的应用报告也非常受欢迎，包括：生物系统的建模和分析，计算机系统编程的安全性，嵌入式系统的建模和分析，中间件和协调语言的规范，程序设计语言语义和实现，静态分析软件和硬件验证，以及特定领域语言和基于模型的工程的语义。
2013-07-26 cs.LO cs.PL
Structured Parallel Programming
基于我们以前对真并发代数律的研究，我们设计了一种结构化真并发并行程序设计语言PPL，与大多数程序设计语言不同的是，PPL有一个显式的并行操作符作为基本操作符，包括它的操作语义、指称语义和公理语义。PPL可以构造一个真正的并发图的范式，这意味着它是可能的，以实现一个编译器的PPL。
2021-11-09 cs.LO
A proof-theoretic view on scheduling in concurrency
本文阐述了一种新的方法的问题的证明理论研究的并发交互称为“证据的时间表”。观察证明理论是非常适合于描述合流系统，而并发具有非确定性作为一个基本特征，我们开发了一个对应的证明提供了什么是需要并发系统合流，即调度。在我们的逻辑系统中，进程和验证者在证明语言的不同片段中显式地显示为证明，并且它们之间的切割消除确实对应于并发系统的执行。这种角色的分离为过程的指称语义提供了新的见解，也为将π演算转换为无前缀的形式主义（如solos）提供了新的方法，作为证明系统之间转换的操作对应物。
2014-09-13 cs.LO
Back to Futures
本文提出一种基于伴随逻辑Curry-Howard解释的并发语言，通过添加三个原子原语编码顺序组合与同步，统一表达期货、分叉/连接并行和单子并发，并形式化线性期货。
2020-10-27 cs.LO cs.PL
Proceedings Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics
本卷包含第25届并发表达性国际研讨会和第15届结构操作语义研讨会（EXPRESS/SOS 2018）的会议记录，该研讨会于2018年9月3日在中国北京举行，作为第29届并发理论国际会议CONCUR 2018的附属研讨会。EXPRESS研讨会旨在汇集对各种形式系统和语义概念的表达感兴趣的研究人员，特别是在并发领域。传统上，他们的重点是比较编程概念（如并发、函数、命令、逻辑和面向对象编程）和计算的数学模型（如进程代数、Petri网、事件结构、模态逻辑和重写系统）之间的相对表达能力。SOS研讨会的目的是成为一个论坛的研究人员，学生和从业人员感兴趣的新发展，未来的调查方向，在结构操作语义领域。SOS研讨会系列的具体目标之一是在从事SOS理论和实践工作的并发和程序设计语言社区之间建立协同作用。自2012年以来，EXPRESS和SOS社区组织了一个年度EXPRESS/SOS联合研讨会，讨论计算数学模型的表达能力以及系统和编程概念的形式语义。
2018-08-24 cs.LO cs.PL
Context-Dependent Effects and Concurrency in Guarded Interaction Trees
IT University of Copenhagen（哥本哈根IT大学）；Univ Lyon, ENS de Lyon, UCBL, CNRS, Inria, LIP, UMR 5668, F-69342, Lyon CEDEX 07（里昂大学，里昂高等师范学校，里昂第一大学，法国国家科学研究中心，Inria，LIP实验室）；University of Groningen（格罗宁根大学）；Aarhus University（奥胡斯大学）
本文提出了一种扩展守卫交互树的方法，以支持依赖上下文的效果和抢占式并发的推理与表示。
2025-12-12 cs.LO cs.PL
Static Race Detection and Mutex Safety and Liveness for Go Programs (extended version)
Go是一种流行的并发程序设计语言，这要归功于它能够有效地结合并发和系统编程。在Go程序中，许多并发错误可能是由数据竞争和通信问题引起的。在本文中，我们开发了一种基于行为类型的理论来静态检测Go程序中的数据竞争和死锁。我们首先使用Go内存模型中定义的happens-before关系，在Go程序模型上指定锁安全性、活动性和数据竞争属性。我们表示这些属性的程序中的$μ$演算模型的类型，并验证它们使用类型级别的模型检查。然后，我们扩展了框架，以考虑Go的通道，并实现了一个静态验证工具，可以检测并发错误。据我们所知，这是Go语言的第一个此类静态验证框架，统一分析了由共享内存访问和异步消息传递通信混合引起的并发错误。
2021-11-18 cs.LO cs.PL
Between quantum logic and concurrency
我们从定义在一种特殊的偏序集（称为因果网）的元素上的两个闭包算子开始。因果网用于模拟并发进程的历史，记录局部状态和事件的发生。如果这样的偏序集的每个极大链（线）满足每个极大反链（割），则这两个闭包算子重合，并生成一个完备的正交模格。在本文中，我们回顾，在这个格中的任何封闭的集合，每一条线满足它或它的正交补在格中，并表明，任何线，在格上的二值状态可以相关联。从这个结果开始，我们描绘了一种逻辑语言，其公式在因果网的闭集上进行解释，其中每行都诱导公式的真值分配。由此产生的逻辑是非经典的，我们表明，最大的反链在因果网相关联的布尔（因此“经典”）子结构的整体量子逻辑。
2014-08-01 cs.DM cs.LO
Proceedings Sixth Workshop on Structural Operational Semantics
本卷包含SOS 2009的会议记录，第六届结构操作语义研讨会于2009年8月31日在意大利博洛尼亚举行，作为CONCUR 2009的附属研讨会，第20届国际并发理论会议。结构操作语义（SOS）是一种为编程和规约语言定义操作语义的技术。该研讨会是研究人员，学生和从业人员感兴趣的新发展和未来的调查方向在SOS领域的论坛。研讨会的具体目标之一是为并发和程序设计语言社区提供一个聚会点。另一个目标是在全世界的研究生和年轻研究人员中传播SOS的理论和实践。
2010-02-15 cs.LO cs.PL
Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems
independent researcher（独立研究员）
针对多智能体LLM系统，形式化四种并发异常并建立一致性层级，通过Verus验证检测器正确性，并在Rust运行时中实现预防。
2026-06-17 cs.DC cs.LG 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
The Topological and Logical Structure of Concurrency and Dependency via Distributive Lattices
本文的动机是希望研究包管理使用的工具包的语义的函数式语言。正如它所揭示的那样，这与并发计算的语义密切相关。我们制作的模型不仅具有理论意义，而且可以进行分析和计算。这项工作作出了一些相关的贡献。首先，它涉及分支依赖结构的规范，存在于从知识表示到包管理的领域，并发计算的语义规范。其次，它以精确的方式将依赖结构与格相关联，与特定的格子类建立完全对应。然后，它利用这一点作为一个关键的成分，再加上未得到充分重视的Bruns-Lakser完成，在相关的依赖结构，以区域设置-对象配备了拓扑和逻辑属性。然后，它提供了一个例子，说明这种属性的相互作用是如何使用的-使用依赖结构的拓扑属性来为相关区域设置的内部逻辑配备表示收缩关系（即“版本控制”）的模态。这种方法让我们看到链接（或者更确切地说，选择链接的对象，即“解决”）作为一种效果。最后，它讨论了这种结构可能涉及到复杂性理论中的重要问题，包括可满足性问题的解决方案。在此过程中，我们将看到这种方法如何与熟悉的对象相关，例如包版本策略，Merkle树，nix操作系统和分布式版本控制工具，如git。
2020-04-12 cs.LO math.LO
Interpreting a concurrent $λ$-calculus in differential proof nets (extended version)
在本文中，我们将展示如何解释一种具有并发性，引用和复制的语言到证明网中，这对应于微分线性逻辑的一个片段。我们证明了一个模拟和充分性定理。在我们的翻译中的一个关键因素是路由区域，一个家庭的网络用于实现通信原语，我们定义和详细研究。
2021-02-10 cs.LO
Verifying that a compiler preserves concurrent value-dependent information-flow security
通常通过对源代码进行推理来证明程序不会泄漏敏感数据。但是这样做在推理和现实之间留下了一个缺口，只能通过解释编译器的行为来填补。当程序强制执行值相关的信息流安全属性（其中位置的分类可以根据其他位置中的值而变化）时，此任务是复杂的，并且当程序利用共享变量并发时进一步复杂化。先前的工作已经正式定义了并发感知的概念，以保持值依赖的安全属性的细化。然而，这个概念要比标准的精化定义复杂得多，标准的精化定义通常应用于编译器对语义保持的验证。到目前为止，还不清楚它是否可以应用于一个现实的编译器，因为不存在一般的分解原则，将其分为更小，更熟悉，证明义务。在这项工作中，我们提供了这样一个分解原则，我们表明，几乎可以一半的复杂性证明安全的细化。此外，我们证明了它的适用性，安全编译，通过证明在伊莎贝尔/HOL的保存值依赖的安全性的概念证明编译器从一个命令式的，而语言到一个通用的RISC风格的汇编语言，为程序与共享内存并发介导的锁定原语。最后，我们执行我们的编译器在伊莎贝尔的跨域桌面合成器的语言模型，展示了我们的知识，第一次使用的编译器验证结果进行信息流的安全属性到一个非平凡的并发程序的汇编级模型。
2019-07-01 cs.CR cs.LO cs.PL
