We present guarded interaction trees -- a structure and a fully formalized framework for representing higher-order 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.

翻译：我们提出守护交互树——一种结构及完整形式化框架，用于在Coq中表示具有高阶效应的高阶计算，其灵感来源于域理论与近期提出的交互树。我们还提出了一种用于推理守护交互树的配套分离逻辑。为证明守护交互树为带效应的高阶语言解释提供了便捷域，我们定义了类PCF语言带效应的解释，并证明该解释是可靠且计算充分的；后者通过基于分离逻辑定义的逻辑关系完成证明。守护交互树还使得不同效应的组合与模块化推理成为可能。为阐明此点，我们给出跨语言交互的类型可靠性模块化证明，用于支持不同高阶语言与不同效应的安全互操作。本文所有结果均在Coq中通过守护类型论上的Iris逻辑完成形式化。