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.
Thu 18 JanDisplayed time zone: London change
09:00 - 10:20 | |||
09:00 20mTalk | On Model-Checking Higher-Order Effectful Programs POPL | ||
09:20 20mTalk | Explicit Effects and Effect Constraints in ReML POPL Martin Elsman University of Copenhagen, Denmark Link to publication DOI | ||
09:40 20mTalk | Decalf: A Directed, Effectful Cost-Aware Logical Framework POPL Harrison Grodin , Jonathan Sterling University of Cambridge, Yue Niu Carnegie Mellon University, Robert Harper Carnegie Mellon University Pre-print | ||
10:00 20mTalk | Modular Denotational Semantics for Effects with Guarded Interaction TreesDistinguished PaperRemote POPL Daniel Frumin University of Groningen, Amin Timany Aarhus University, Lars Birkedal Aarhus University DOI Pre-print |