paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Familial monads and structural operational semantics

Familial monads 与结构化操作语义
POPL 3(POPL)2019匹配度 2/10 · 该论文属于纯PL理论（范畴论、结构化操作语义、互模拟），不涉及LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析，与用户画像中AI与PL交叉的核心方向无直接关联。虽然形式语义是PL基础，但缺乏AI/LLM元素或工业落地案例。引用 5 inbox
Tom Hirschowitz
形式语义并发、并行与内存模型
crossref: 2026-09-10

AI 速览

一句话：提出 familial monad 范畴框架，统一结构化操作语义，并证明互模拟同余与上下文互模拟可靠性。

本文针对结构化操作语义（SOS）缺乏统一范畴论基础的问题，提出以 familial monads 为核心的范畴框架，用单子结构刻画 SOS 规则及其行为。作者在合适的假设下证明互模拟（bisimilarity）是上下文同余，并进一步细化该框架，证明“上下文互模拟”（bisimulation up to context）方法的可靠性；该方法可显著缩小互模拟关系，从而简化证明。为展示框架的灵活性，作者在三种 π-演算变体中重新证明了已有结果，说明该范畴方法能统一处理不同演算的语义与互模拟性质。

问题
如何为结构化操作语义提供统一的范畴论基础，并在一般条件下判定互模拟是否为同余，同时支持更高效的互模拟证明方法。
方法
引入 familial monads 的范畴框架，将 SOS 规则编码为单子结构；在该框架下给出充分条件证明互模拟同余，并细化框架以证明上下文互模拟的可靠性。
评估
通过在三种 π-演算变体中重新证明已知结果，展示该框架对不同演算语义与互模拟性质的灵活性与适用性。
原文摘要（Abstract）

We propose a categorical framework for structural operational semantics, in which we prove that under suitable hypotheses bisimilarity is a congruence. We then refine the framework to prove soundness of bisimulation up to context, an efficient method for reducing the size of bisimulation relations. Finally, we demonstrate the flexibility of our approach by reproving known results in three variants of the π-calculus.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@article{paperbot660,
  title = {Familial monads and structural operational semantics},
  author = {Tom Hirschowitz},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {POPL},
  year = {2019},
  doi = {10.1145/3290334}
}