一句话：提出 EffHOL，将句法可实现性推广到带副作用的计算，并通过 monad 参数化抽取效应化实者。
句法可实现性把命题解释为计算实者的规约，但传统框架主要处理纯计算，难以统一支持副作用。本文提出 EffHOL，一个将句法可实现性扩展到现代编程范式的框架。EffHOL 结合高阶多态，以支持高阶命题实者的类型化，并采用 monad 表示和推理效应计算。作者构造从直觉主义高阶逻辑到 EffHOL 的句法可实现性翻译，通过构造性可靠性证明抽取可计算实者。由于以 monad 参数化，EffHOL 能为纯 HOL 不可证的命题合成效应化实者，并以 continuations 和 memoization 等例子说明其统一不同计算模型的能力；语义上，任一 EffHOL 实例诱导 evidenced frame，进而得到 tripos 与可实现性 topos。
Realizability interprets propositions as specifications for computational entities in programming languages. Specifically, syntactic realizability is a powerful machinery that handles realizability as a syntactic translation of propositions into new propositions that describe what it means to realize the input proposition. This paper introduces EffHOL (Effectful Higher-Order Logic), a novel framework that expands syntactic realizability to uniformly support modern programming paradigms with side effects. EffHOL combines higher-kinded polymorphism, enabling typing of realizers for higher-order propositions, with a computational term language that uses monads to represent and reason about effectful computations. We craft a syntactic realizability translation from (intuitionistic) higher-order logic (HOL) to EffHOL, ensuring the extraction of computable realizers through a constructive soundness proof. EffHOL’s parameterization by monads allows for the synthesis of effectful realizers for propositions unprovable in pure HOL, bridging the gap between traditional and effectful computational paradigms. Examples, including continuations and memoization, showcase EffHOL’s capability to unify diverse computational models, with traditional ones as special cases. For a semantic connection, we show that any instance of EffHOL induces an evidenced frame, which, in turn, yields a tripos and a realizability topos.