一句话：引入答案类型修改限制，使带代数效应处理器的高阶程序模型检测可判定，并实现验证器 EffCaml。
自 Ong 的开创性工作以来，高阶模型检测（HOMC）受到关注，而将其应用于实际软件需处理计算效应。Dal Lago 与 Ghyselen 研究了 HOMC 对代数效应处理器的扩展，但给出了不可判定性结果。本文探索可确保 HOMC 可判定、同时允许实现多种效应的程序限制。作者将不可判定性的症结归结为可同时活跃的代数效应处理器数量无界，为此引入答案类型修改（ATM），以约束同时活跃的处理器数量。论文证明 ATM 可保证 HOMC 可判定，并说明其能容纳广泛的效应。为评估方法，作者实现自动验证器 EffCaml，确认文中讨论的程序实例均可自动验证。
Since the seminal work by Ong, the model checking of higher-order programs—called higher-order model checking , or HOMC for short—has gained attention. It is also crucial for making HOMC applicable to real-world software to address programs involving computational effects. Recently, Dal Lago and Ghyselen considered an extension of HOMC to algebraic effect handlers , which enable programming the semantics of effects. They showed a negative result for HOMC with algebraic effect handlers—it is undecidable. In this work, we explore a restriction on programs with algebraic effect handlers which ensures the decidability of HOMC while allowing implementations of various effects. We identify the crux of the undecidability as the use of an unbounded number of algebraic effect handlers being active at the same time. To prevent it, we introduce answer-type modification (ATM), which can bound the number of algebraic effect handlers that can be active at the same time. We prove that ATM can ensure the decidability of HOMC and show that it accommodates a wide range of effects. To evaluate our approach, we implemented an automated verifier EffCaml based on the presented techniques and confirmed that the program examples discussed in this paper can be automatically verified.
@article{Sekiyama024,
title = {Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification},
author = {Taro Sekiyama and Hiroshi Unno},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689805}
}