Complete First-Order Reasoning for Properties of Functional Programs

Adithya Murali, Lucas Peña, Ranjit Jhala, P. Madhusudan

Research output: Contribution to journalArticlepeer-review

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 languageEnglish (US)
Article number259
JournalProceedings of the ACM on Programming Languages
Volume7
Issue numberOOPSLA2
DOIs
StatePublished - 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

Fingerprint

Dive into the research topics of 'Complete First-Order Reasoning for Properties of Functional Programs'. Together they form a unique fingerprint.

Cite this