一句话：提出 omni-big-step 与 omni-small-step 语义，用「状态到结果集合」的推导统一刻画非确定性与未定义行为，并内蕴安全性。
传统小步/大步操作语义的每条推导只描述单条执行路径，因此面对非确定性以及可能卡住（未定义行为）时，需要额外安全判定或错误标记。本文深入阐述 omni-big-step 与 omni-small-step 两种语义风格：它们把起始状态与「结果集合」而非单个结果相关联，从而用单条推导覆盖程序所有可能的非确定执行，并天然断言安全性（保证任何执行分支都不会卡住）。作者指出 omni 语义可理解为归纳定义的最弱前置条件（更一般地，谓词变换器）语义，但不同于通常的 WP，它不需循环/递归不变式，而是像传统小步/大步语义那样使用展开规则。文章还探讨了若干新应用：lambda 演算的类型安全证明、部分正确性推理，以及将终止但可能非确定的源程序编译到非确定目标语言时的前向编译正确性证明。所有结果均在 Coq 中形式化。
This article gives an in-depth presentation of the omni-big-step and omni-small-step styles of semantic judgments. These styles describe operational semantics by relating starting states to sets of outcomes rather than to individual outcomes. A single derivation of these semantics for a particular starting state and program describes all possible nondeterministic executions (hence the name omni ), whereas in traditional small-step and big-step semantics, each derivation only talks about one single execution. This restructuring allows for straightforward modeling of both nondeterminism and undefined behavior as commonly encountered in sequential functional and imperative programs. Specifically, omnisemantics inherently assert safety (i.e., they guarantee that none of the execution branches gets stuck), while traditional semantics need either a separate judgment or additional error markers to specify safety in the presence of nondeterminism. Omnisemantics can be understood as an inductively defined weakest-precondition semantics (or more generally, predicate-transformer semantics) that does not involve invariants for loops and recursion but instead uses unrolling rules like in traditional small-step and big-step semantics. Omnisemantics were previously described in association with several projects, but we believe the technique has been underappreciated and deserves a well-motivated, extensive, and pedagogical presentation of its benefits. We also explore several novel aspects associated with these semantics, in particular, their use in type-safety proofs for lambda calculi, partial-correctness reasoning, and forward proofs of compiler correctness for terminating but potentially nondeterministic programs being compiled to nondeterministic target languages. All results in this article are formalized in Coq.
@article{paperbot2136,
title = {Omnisemantics: Smooth Handling of Nondeterminism},
author = {Arthur Charguéraud and Adam Chlipala and Andres Erbsen and Samuel Gruetter},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {1},
year = {2023},
doi = {10.1145/3579834}
}