Answer Refinement Modification: Refinement Type System for Algebraic Effects and...
summary
Proposes a refinement type system that tracks how delimited-continuation effects change return types via answer refinement modification, formalizes ATM/ARM, and proves soundness; implements a type checker and inference algorithm for a subset of OCaml 5 with effect handlers and runs benchmarks showing more precise types (e.g., proving exact list results and max-of-two for nondeterminism) and practical usefulness; also gives a CPS transform that is bidirectionally refinement‑type‑preserving and discusses tradeoffs (annotations, less readable inferred types).
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:17Algebraic effects and handlers
- 4:12Refinement types intro
- 5:19Type system design
- 7:03Answer type modification
- 10:16Modification in practice
- 11:44Formal syntax and reasoning
- 14:10Typing examples
- 15:40Advanced features
- 16:02Q&A
related talks
22mHigher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification
29mExplicit Refinement Types
16mA Hoare-Logic Style Refinement Types Formalisation
14mOn Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
29mMechanized monadic equational reasoning for ML references
19mTowards a Reflection for Effect Handlers
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
56mOn Type-Based Techniques for Program Manipulation