Fri 20 Jan 2023 09:25 - 09:50 at Square - Logic & Decidability II Chair(s): Joost-Pieter Katoen

The monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in static analysis and verification. We propose a new class of higher-order Horn constraints which extend MSL to higher-order logic and develop a resolution-based decision procedure. Higher-order MSL Horn constraints can quite naturally capture the complex patterns of call and return that are possible in higher-order programs, which make them well suited to higher-order program verification. In fact, we show that the higher-order MSL satisfiability problem and the HORS model checking problem are interreducible, so that higher-order MSL can be seen as a constraint-based approach to higher-order model checking. Finally, we describe an implementation of our decision procedure and its application to verified socket programming.

Fri 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:15
Logic & Decidability IIPOPL at Square
Chair(s): Joost-Pieter Katoen RWTH Aachen University
09:00
25m
Talk
When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
POPL
Zachary Kincaid Princeton University, Nicolas Koh Princeton University, Shaowei Zhu Princeton University
DOI
09:25
25m
Talk
Higher-Order MSL Horn Constraints
POPL
Jerome Jochems University of Bristol, Eddie Jones University of Bristol, Steven Ramsay University of Bristol
DOI
09:50
25m
Talk
Fast Coalgebraic Bisimilarity Minimization
POPL
Jules Jacobs Radboud University Nijmegen, Thorsten Wissmann Radboud University Nijmegen
DOI Pre-print