一句话：在范畴框架中定义替换封闭互模拟，并用 Howe 方法证明其同余性。
本文引入一个用于操作语义的范畴框架，在其中定义替换封闭互模拟（substitution-closed bisimilarity），它可视为 Abramsky 应用互模拟开放扩张的抽象类比。作者沿用 Howe 方法证明该互模拟满足同余定理，从而为抽象操作语义提供组合式推理工具。作为中间结果，他们将 Fiore 等人关于带变量绑定语法的标准框架推广到 skew-monoidal 情形，以支撑框架的形式化构造。最后展示该框架能覆盖大步风格下的 call-by-name 与 call-by-value λ-演算，说明其适用性。
We introduce a categorical framework for operational semantics, in which we define substitution-closed bisimilarity, an abstract analogue of the open extension of Abramsky's applicative bisimilarity. We furthermore prove a congruence theorem for substitution-closed bisimilarity, following Howe's method. We finally demonstrate that the framework covers the call-by-name and call-by-value variants of λ-calculus in big-step style. As an intermediate result, we generalise the standard framework of Fiore et al. for syntax with variable binding to the skew-monoidal case.
DOI 原文 ·
@inproceedings{paperbot5518,
title = {A Cellular Howe Theorem},
author = {Peio Borthelle and Tom Hirschowitz and Ambroise Lafont},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394738}
}