一句话：提出支持答案类型多态与子类型的效应处理演算 HEPCF□ATM，并通过选择性 CPS 变换证明其高阶模型检测可判定。
将高阶模型检测用于效应处理程序面临可判定性障碍：Dal Lago 与 Ghyselen 已证其不可判定，而单态答案类型修改虽可恢复可判定性，却牺牲多态性、模块性与表达力。本文定义同时支持答案类型多态和子类型的演算，并保证其模型检测问题可判定。核心是引入多态答案类型 □，在表达力与可判定性间取得折中；作者通过选择性、类型制导的 CPS 变换，将程序翻译到不含效应处理与多态的目标演算，从而证明可判定性。所提演算 HEPCF□ATM 还允许由尾恢复效应处理器实现的效应具有多态答案类型。作者实现了概念验证模型检测器。
Applying higher-order model checking techniques to programs that use effect handlers is a major challenge, given the recent undecidability result obtained by Dal Lago and Ghyselen. This challenge has been addressed by using answer-type modifications, the use of a monomorphic version of which allows to recover decidability. However, the absence of polymorphism leads to a loss of modularity, reusability, and even expressivity. In this work, we study the problem of defining a calculus that on the one hand supports answer-type polymorphism and subtyping but on the other hand ensures the underlying model checking problem to remain decidable. The solution proposed in this paper is based on the introduction of the polymorphic answer-type □ whose role is to provide a good compromise between expressiveness and decidability, the latter demonstrated through the construction of a selective type-directed CPS transformation targeting a calculus without effect handlers and any form of polymorphism. Noticeably, the introduced calculus HEPCF □ ATM allows the answer types of effects implemented by tail-resumptive effect handlers to be polymorphic. We also implemented a proof-of-concept model checker for HEPCF □ ATM programs.
@article{paperbot2964,
title = {On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs},
author = {Taro Sekiyama and Ugo Dal Lago and Hiroshi Unno},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763184}
}