一句话：提出守卫交互树及其分离逻辑，用于在 Coq 中模块化地给出带高阶效应的语言指称语义并证明类型安全。
论文针对高阶语言中高阶效应的指称语义与模块化推理问题，提出“守卫交互树”（guarded interaction trees）：一种受域理论和 interaction trees 启发、在 Coq 中完全形式化的结构，用于表示带高阶效应的计算。作者还给出配套的分离逻辑，并用它定义逻辑关系。为验证该语义域，作者解释了一个带效应的 PCF 类语言，证明解释是可靠且计算充分的，并用分离逻辑定义的逻辑关系证明计算充分性。该框架支持不同效应的组合与模块化推理，文中给出不同高阶语言跨语言安全互操作的模块化类型可靠性证明。所有结果均在 Coq 的 Iris 逻辑与守卫类型论中形式化。
We present guarded interaction trees — a structure and a fully formalized framework for representing higherorder computations with higher-order effects in Coq, inspired by domain theory and the recently proposed interaction trees. We also present an accompanying separation logic for reasoning about guarded interaction trees. To demonstrate that guarded interaction trees provide a convenient domain for interpreting higher-order languages with effects, we define an interpretation of a PCF-like language with effects and show that this interpretation is sound and computationally adequate; we prove the latter using a logical relation defined using the separation logic. Guarded interaction trees also allow us to combine different effects and reason about them modularly. To illustrate this point, we give a modular proof of type soundness of cross-language interactions for safe interoperability of different higher-order languages with different effects. All results in the paper are formalized in Coq using the Iris logic over guarded type theory.
@article{paperbot2597,
title = {Modular Denotational Semantics for Effects with Guarded Interaction Trees},
author = {Dan Frumin and Amin Timany and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632854}
}