Recent years have witnessed the rise of compositional semantics as a foundation for formal verification of complex systems. In particular, interaction trees have emerged as a popular denotational semantics. Interaction trees achieve compositionality by providing a reusable library of effects. However, their notion of effects does not support higher-order effects, i.e., effects that take or return monadic computations. Such effects are essential to model complex semantic features like parallel composition and call/cc. We introduce Higher-Order Interaction Trees (HITrees), the first variant of interaction trees to support higher-order effects in a non-guarded type theory. HITrees accomplish this through two key techniques: first, by designing the notion of effects such that the fixpoints of effects with higher-order input can be expressed as inductive types inside the type theory; and second, using defunctionalization to encode higher-order outputs into a first-order representation. We implement HITrees in the Lean proof assistant, accompanied by a comprehensive library of effects including concurrency, recursion, and call/cc. Furthermore, we provide two interpretations of HITrees, as state transition systems and as monadic programs. To demonstrate the expressiveness of HITrees, we apply them to define the semantics of a language with parallel composition and call/cc.

翻译：近年来，组合语义学作为复杂系统形式化验证的基础逐渐兴起。其中，交互树已成为一种流行的指称语义。交互树通过提供可复用的效应库实现组合性。然而，其效应概念不支持高阶效应，即接受或返回单子计算的效应。此类效应对于建模并行组合和call/cc等复杂语义特征至关重要。本文提出高阶交互树（HITrees），这是首个在非守卫类型论中支持高阶效应的交互树变体。HITrees通过两项关键技术实现这一目标：首先，通过设计效应概念，使得具有高阶输入的效应不动点可在类型论内表达为归纳类型；其次，利用反函数化将高阶输出编码为一阶表示。我们在Lean证明助手中实现了HITrees，并配备了包含并发、递归和call/cc在内的完整效应库。此外，我们提供了HITrees的两种解释：作为状态转移系统和作为单子程序。为展示HITrees的表达能力，我们将其应用于定义支持并行组合和call/cc的语言语义。