Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers

Explore a groundbreaking 23-minute conference talk from POPL 2024 that introduces a novel refinement type system for languages with algebraic effects and handlers. Delve into the concept of Answer Refinement Modification (ARM), which enables precise tracking of effect occurrence and order in program execution. Learn how this approach addresses the complexities of delimited continuations in algebraic effects and handlers. Discover the formalization of the type system supporting ARM and Answer Type Modification (ATM), and understand its proven soundness. Examine the practical application of this system through its extension to a subset of OCaml 5, complete with type checking and inference algorithm implementation. Compare this direct reasoning approach with an alternative Continuation Passing Style (CPS) transformation method, weighing the pros and cons of each. Gain insights into the challenges and advancements in program verification for languages incorporating algebraic effects and handlers.

[POPL'24] Answer Refinement Modification: Refinement Type System for Algebraic Effects and...