一句话：将高阶代数效应程序归约为高阶递归方案，并刻画效应处理器下模型检测的可判定边界。
本文研究带代数效应的高阶函数程序的模型检测问题。经典结果（Knapik、Ong、Kobayashi 等）表明，高阶类型程序对一元二阶逻辑（MSO）公式的模型检测是可判定的；但加入概率选择、全局存储等代数效应后，已有结果从非确定性效应的正面结论到概率效应下连可达性都不可判定。作者提出一种自然优雅的视角，把产生代数效应的高阶程序视为普通的高阶递归方案（HORS），从而在统一框架下重新审视该问题。随后作者考察效应处理器：证明在一般处理器存在时模型检测问题不可判定，而当处理器具有简单语法形式（仍足以刻画所谓 generic effects）时可判定性得以保持。文中还提示了通用规约语言的可能形态，据此解释文献中已有结果并导出新结论。
Model-checking is one of the most powerful techniques for verifying systems and programs, which since the pioneering results by Knapik et al., Ong, and Kobayashi, is known to be applicable to functional programs with higher-order types against properties expressed by formulas of monadic second-order logic. What happens when the program in question, in addition to higher-order functions, also exhibits algebraic effects such as probabilistic choice or global store? The results in the literature range from those, mostly positive, about nondeterministic effects, to those about probabilistic effects, in the presence of which even mere reachability becomes undecidable. This work takes a fresh and general look at the problem, first of all showing that there is an elegant and natural way of viewing higher-order programs producing algebraic effects as ordinary higher-order recursion schemes. We then move on to consider effect handlers, showing that in their presence the model checking problem is bound to be undecidable in the general case, while it stays decidable when handlers have a simple syntactic form, still sufficient to capture so-called generic effects . Along the way, we hint at how a general specification language could look like, this way justifying some of the results in the literature, and deriving new ones.