Abstract
Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function definitions followed by quantifier-free reasoning using SMT solvers. We uncover foundational theoretical properties of this heuristic, revealing that it can be generalized and formalized as a technique that is in fact complete for reasoning with combined First-Order theories of algebraic datatypes and background theories, where background theories support decidable quantifier-free reasoning. The theory developed in this paper explains the efficacy of these heuristics when they succeed, explain why they fail when they fail, and the precise role that user help plays in making proofs succeed.
Original language | English (US) |
---|---|
Article number | 259 |
Journal | Proceedings of the ACM on Programming Languages |
Volume | 7 |
Issue number | OOPSLA2 |
DOIs | |
State | Published - Oct 16 2023 |
Keywords
- Algebraic Datatypes (ADTs)
- Completeness
- First-Order Logic
- Liquid Haskell
- Natural Proofs
- Refinement Types
- Thrifty Instantiation
ASJC Scopus subject areas
- Software
- Safety, Risk, Reliability and Quality