POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Thu 18 Jan 2024 09:00 - 09:20 at Turing Lecture - Higher-Order Effectful Programs Chair(s): Sam Lindley

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 Jan

Displayed time zone: London change

09:00 - 10:20
Higher-Order Effectful ProgramsPOPL at Turing Lecture
Chair(s): Sam Lindley University of Edinburgh
09:00
20m
Talk
On Model-Checking Higher-Order Effectful Programs
POPL
Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Alexis Ghyselen University of Bologna
09:20
20m
Talk
Explicit Effects and Effect Constraints in ReML
POPL
Martin Elsman University of Copenhagen, Denmark
Link to publication DOI
09:40
20m
Talk
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
20m
Talk
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