Higher-Order Constrained Horn Clauses and Refinement Types

Toby Cathcart Burn, C. -H. Luke Ong, Steven J. Ramsay

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 proble…