On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
summary
Claims decidability for a nontrivial fragment of effectful higher-order programs by introducing polymorphic answer-type □ and a type system that allows unbounded tail-resumptive handlers but statically bounds non-tail resumptive uses. Proof proceeds by a selective type-directed CPS transformation to a handler-free EPcf where higher-order model checking is decidable. Implements a proof-of-concept model checker for HEPCF□ATM, ships artifacts, and verifies small benchmarks (microbenchmarks complete quickly), with formal reductions and mechanized results.
AI-written summary · about
chapters (7)
- 0:00Higher-order model checking intro
- 3:11Model checking with effect handlers
- 6:22Effect handlers decidability
- 7:27Decidable fragment for model checking
- 11:02Type system for decidable class
- 12:06Implementation benchmarks
- 12:53Q&A
related talks
22mHigher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...
15mEffect Handlers, Evidently
12mTowards Dependently-Typed Control Effects (Extended Abstract)
17mHefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
16mContextual Effect Polymorphism Meets Bidirectional Effects (Extended Abstract)
19mTowards a Reflection for Effect Handlers
29mHigher-Order Weakest Precondition Transformers via a CPS Transformation