Lab Lunch by Danel Ahman
What 


When 
May 05, 2015 from 01:00 PM to 02:00 PM 
Where  MF2 
Add event to calendar 
vCal iCal 
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 typeandeffect systems, Hoare types, trace effects and protocol specifications.
I'll also present a corresponding refinementtyped version of Levy's CallByPushValue language that incorporates the effect refinements in its computation types. We give this language a 2level 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 effectdependent optimizations.