On Model-Checking Higher-Order Effectful Programs (Long Version)

TL;DR

This paper investigates the model-checking problem for higher-order effectful programs, revealing decidability boundaries and proposing a natural scheme to view such programs as recursion schemes, with implications for verification techniques.

Contribution

It introduces a novel perspective by viewing effectful higher-order programs as recursion schemes and analyzes the decidability of model checking with effect handlers.

Findings

Model checking is decidable for effectful programs with simple handlers.

General effect handlers lead to undecidability in model checking.

A framework for a potential specification language is proposed.

Abstract

Model-checking is one of the most powerful techniques for verifying systems and programs, which since the pioneering results by Knapik et al., Ong, and Kobayashi, is known to be applicable to functional programs with higher-order types against properties expressed by formulas of monadic second-order logic. What happens when the program in question, in addition to higher-order functions, also exhibits algebraic effects such as probabilistic choice or global store? The results in the literature range from those, mostly positive, about nondeterministic effects, to those about probabilistic effects, in the presence of which even mere reachability becomes undecidable. This work takes a fresh and general look at the problem, first of all showing that there is an elegant and natural way of viewing higher-order programs producing algebraic effects as ordinary higher-order recursion schemes. We then move on to consider effect handlers, showing that in their presence the model checking problem is bound to be undecidable in the general case, while it stays decidable when handlers have a simple syntactic form, still sufficient to capture so-called generic effects. Along the way we hint at how a general specification language could look like, this way justifying some of the results in the literature, and deriving new ones.