Higher-Order Constrained Horn Clauses for Verification

Explore a 25-minute conference presentation from POPL 2018 that delves into the development of higher-order constrained Horn clauses for automated verification of higher-order functional programs. Learn about the innovative approach to establishing canonical models through monotone logic program reduction, despite the absence of least models in satisfiable higher-order clause systems. Discover how refinement type systems can be implemented to automate model searches and express term properties within the higher-order constrained Horn clause framework. Presented by researchers from the University of Oxford and University of Bristol, this talk introduces fundamental concepts in program verification, including constrained Horn clauses, refinement types, and higher-order logic.