Higher-order constrained horn clauses for verification

Journal article

Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision problem concerning their satisfiability. We show that, although satisfiable systems of higher-order clauses do not generally have least models, there is a notion of canonical model obtained through a reduction to a problem concerning a kind of monotone logic program. Following work in higher-order program verification, we develop a refinement type system in order to reason about and automate the search for models. This provides a sound but incomplete method for solving the decision problem. Finally, we show that there is a sense in which we can use refinement types to express properties of terms whilst staying within the higher-order constrained Horn clause framework.

Authors: Cathcart Burn, T; Ong, C; Ramsay, S

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Association for Computing Machinery
• Journal: Proceedings of the ACM on Programming Languages
• Volume: 2
• Pages: 11
• Publication date: 2017-12-01
• Acceptance date: 2017-10-30
• DOI: 10.1145/3158099
• EISSN: 2475-1421
• Language: English
• Keywords: types; higher-order program verification; constrained Horn clauses