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}
}