Personal tools
You are here: Home Events Lab Lunch by Danel Ahman

Lab Lunch by Danel Ahman

— filed under:

  • Lab Lunch
When May 05, 2015
from 01:00 PM to 02:00 PM
Where MF2
Add event to calendar vCal

Refinement Types for Algebraic Effects



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.

Document Actions