一句话：提出模块化并发语言语义，将局部抽象求值与全局具体组合分离，以声明式刻画并发模型并支持程序逻辑。
并发程序的形式化推理需要严格且与程序逻辑相匹配的语义。本文提出一种模块化的并发编程语言语义，将表达式和语句的局部求值置于抽象符号环境中，再将其组合为全局计算并具体化，从而可增量加入新语言概念而无需修改框架。其基础是推广程序 trace：用事件描述符和尾部续延标记丰富演化状态序列，使调度约束从局部求值推迟到全局组合阶段；通过事件结构上的良构性谓词声明式刻画多种并发模型。文中还展示了如何为该语义定义可靠的程序逻辑与演算。
Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. We propose a novel modular semantics designed to align smoothly with program logics used in deductive verification and formal specification of concurrent programs. Our semantics separates local evaluation of expressions and statements performed in an abstract, symbolic environment from their composition into global computations, at which point they are concretised. This makes incremental addition of new language concepts possible, without the need to revise the framework. The basis is a generalisation of the notion of a program trace as a sequence of evolving states that we enrich with event descriptors and trailing continuation markers. This allows to postpone scheduling constraints from the level of local evaluation to the global composition stage, where well-formedness predicates over the event structure declaratively characterise a wide range of concurrency models. We also illustrate how a sound program logic and calculus can be defined for this semantics.
@article{paperbot2678,
title = {Locally Abstract, Globally Concrete Semantics of Concurrent Programming Languages},
author = {Crystal Chang Din and Reiner Hähnle and Ludovic Henrio and Einar Broch Johnsen and Violet Ka I Pun and S. Lizeth Tapia Tarifa},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {46},
number = {1},
year = {2024},
doi = {10.1145/3648439}
}