Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification
summary
Claims decidability for higher-order model checking of programs with algebraic effect handlers by statically bounding the number of simultaneously active handlers via answer-type modification (ATM), shows the undecidability stems from encoding naturals using unbounded handlers and prevents that by bounding reachable predecessors, proves decidability via a CPS/shift-style transformation, implements an automated tool EffCaml verifier, and reports small example checks (exceptions, local store, backtracking) as promising though not yet scaled.
AI-written summary · about
chapters (6)
- 0:00Higher-order model checking intro
- 2:28Effectful programs in model checking
- 4:16Decidable fragment with answer-type mod
- 12:55Answer types and restrictions
- 16:54Conclusion and future directions
- 17:19Q&A
related talks
14mOn Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...
17mHefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
22mType-Safe Code Generation With Algebraic Effects and Handlers
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
16mAn Intrinsically Typed Compiler for Algebraic Effect Handlers
19mTowards a Reflection for Effect Handlers
12mTowards Dependently-Typed Control Effects (Extended Abstract)