一句话：在高阶纯函数式语言中借助 Extended EPR 与关系抽象实现可判定、支持量词的程序验证，并用三值逻辑隐藏编码复杂性。
可判定自动化使程序验证工具更易被非专家使用，但可判定逻辑片段限制强，而 Extended EPR 与关系抽象虽能处理量词和未解释函数，其编码复杂且不完备。本文把 Extended EPR 与关系抽象引入高阶纯函数式语言：以偏函数定义语言语义，由此得到行为良好的三值逻辑，既匹配关系抽象编码的行为，又隐藏其复杂性。原型实现表明，该语言能符合人体工学地复现基于 EPR 的验证基准，并验证归纳数据类型上的递归程序。
Decidable automation is a key feature of program verification tools, which makes them easier for non-expert developers to use and understand. Unfortunately, decidable fragments of logic are very restrictive, and not ideal for the expression of idiomatic programs. The decidable Extended EPR fragment, combined with an encoding technique called relational abstraction , has seen wide use for its ability to handle both quantifiers and uninterpreted functions. However, the complexity of the relational abstraction encoding, combined with its inherent incompleteness, still poses a significant obstacle to non-experts. In this paper, we show that Extended EPR and relational abstraction can be deployed to achieve decidable, quantified verification within a familiar, principled domain: a higher-order, purely-functional programming language. We observe that, by defining the semantics of our language in terms of partial functions, we obtain a well-behaved, three-valued logic that matches the behavior of the relational abstraction encoding while hiding its complexity. We demonstrate that our prototype implementation can ergonomically replicate EPR-based program verification benchmarks and verify recursive programs on inductive datatypes.
@article{paperbot3787,
title = {Effectively Propositional Higher-Order Functional Programming},
author = {Nicholas V. Lewchenko and Kunha Kim and Bor-Yuh Evan Chang and Gowtham Kaki},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798259}
}