POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 16:55 - 17:20 at Amphitheater 44 - Logic Chair(s): Alexandra Silva

We study the relationship between two kinds of higher-order extensions of model checking: HORS model checking, where models are extended to higher-order recursion schemes, and HFL model checking, where the logic is extedned to higher-order fixpoint logic. Those extensions have been independently studied until recently, and the former has been applied to higher-order program verification. We show that there exist (arguably) natural reductions between the two problems. To prove the correctness of the translation from HORS to HFL model checking, we establish a type-based characterization of HFL model checking, which should be of independent interest. The results reveal a close relationship between the two problems, enabling cross-fertilization of the two research threads.

Wed 18 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:30 - 17:45
LogicPOPL at Amphitheater 44
Chair(s): Alexandra Silva University College London
16:30
25m
Talk
Monadic second-order logic on finite sequences
POPL
Loris D'Antoni University of Wisconsin–Madison, Margus Veanes Microsoft Research
16:55
25m
Talk
On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
POPL
Naoki Kobayashi University of Tokyo, Japan, Etienne Lozes ENS Cachan, Florian Bruse University of Kassel
17:20
25m
Talk
Coming to Terms with Quantified Reasoning
POPL
Simon Robillard Chalmers University of Technology, Andrei Voronkov University of Manchester, Laura Kovacs Chalmers University of Technology