一句话：提出 PLEX，在 PLE 基础上支持 η-展开、β-归约与依赖模式匹配的符号求值，弥补精化类型与一阶 SMT 求解器间的高阶推理缺口。
精化类型常借助 SMT 求解器来自动化程序验证，但 SMT 求解器是一阶的，无法验证需要高阶推理的性质。Proof by Logical Evaluation（PLE）在精化类型与 SMT 求解器之间提供了一层符号求值能力，但不支持高阶推理。本文提出 PLEX，作为 PLE 的扩展，支持 η-展开、β-归约以及依赖模式匹配。作者证明了 PLEX 的可靠性与终止性，并在 Liquid Haskell 中实现了该算法。评估表明，PLEX 能处理那些必须使用高阶数据、因而 PLE 无法处理的示例。该算法通过精化类型弥合了高阶语言与一阶 SMT 求解器之间的鸿沟。
Refinement types often use SMT solvers to automate program verification. However, since SMT solvers are first-order, verification of properties that requires higher-order reasoning is not possible. Proof by Logical Evaluation (PLE) is an algorithm that provides a layer between refinement types and SMT solvers that permits symbolic evaluation of functions, but it lacks support for higher-order reasoning. We introduce PLEX, an extension to PLE, that supports η -expansions, β -reductions, and dependent pattern matching. We prove that PLEX is sound and terminating, describe its implementation in Liquid Haskell, and evaluate it on examples that make essential use of higher-order data, and as such they cannot be handled by PLE. The new PLEX algorithm bridges the gap between higher-order languages and first-order SMT solvers via refinement types.
@article{paperbot3845,
title = {PLEX: Normalization for Refinement Types},
author = {Alessio Ferrarini and Niki Vazou and Wouter Swierstra},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798248}
}