Automated Temporal Verification for Algebraic Effects
summary
ContEffs provides a regular-expression–based logic to state precise temporal properties for algebraic effects and a forward verifier plus fixpoint calculator that emits proof obligations discharged by Z3 (pure facts) and a term-rewriting backend for regular-expression inclusion; the prototype (OCaml/Multicore-style core) supports zero-shot, one-shot and multi-shot continuations, proves soundness, infers omega traces to flag potential nontermination, and on synthetic benchmarks shows term-rewriting disproves inclusions faster than proving; current gap: no built-in heap/separation reasoning.
AI-written summary · about
chapters (17)
- 0:00Algebraic effects intro
- 1:02Algebraic effects examples
- 4:11Effectful control flow challenges
- 8:25Temporal verification approach
- 9:49Core language design
- 11:36File handling specs
- 14:09Reasoning at handlers
- 17:14Multi-shot continuations
- 19:22Evaluation benchmarks
- 20:30Conclusion and future work
- 21:46Q&A
- 23:11Core language clarifications
- 23:53Effect type systems comparison
- 24:34Spec inference with input
- 25:21Error messages benefits
- 26:26Applications beyond verification
- 27:28Future work: grammars