Refinement Types for Algebraic Effects
Abstract:
I'll talk about some investigations into an algebraic treatment of refinement types for languages with computational effects.
I'll show how describing computational effects using algebraic theories (following Plotkin and Power) induces a small modal logic (of effect refinements) for reasoning about sets of equivalence classes of computation trees. In this way one can account for seemingly different effect specifications found in the literature, such as, annotations in type-and-effect systems, Hoare types, trace effects and protocol specifications.
I'll also present a corresponding refinement-typed version of Levy's Call-By-Push-Value language that incorporates the effect refinements in its computation types. We give this language a 2-level semantics using suitable bifibrations and general fibred adjunctions.
Finally, we also demonstrate how this language can be used to validate programs against effect specifications and how it can be used to validate effect-dependent optimizations.