LFCS seminar: Danel Ahman: A fibrational view on computational effects
What 


When 
Nov 28, 2017 from 04:00 PM to 05:00 PM 
Where  IF 4.31/4.33 
Add event to calendar 
vCal iCal 
In this talk I will give an overview of some of the work I did during my PhD. Specifically, I will present my work on the interplay between dependent types and computational effects, both from a (fibrational) categorytheoretic viewpoint and from a lambdacalculus viewpoint.
First, I will show that similarly to the wellknown results from the simply typed setting, computational effects can be modelled uniformly using monads and adjunctions also in the dependently typed setting. In particular, instead of using monads and adjunctions on categories (modelling simple types), one switches to monads and adjunctions on (split) fibrations (modelling dependent types). In the talk I will also discuss various examples of such fibrational models, e.g., based on families fibrations and liftings of adjunctions; simple fibrations and models of Egger et al.'s Enriched Effect Calculus; EilenbergMoore resolutions of split fibred monads; and the fibration of continuous families of cpos and liftings of CPOenriched adjunctions.
From a lambdacalculus viewpoint, I will present a natural extension of vanilla Type Theory with computational effects that is sound and complete with respect to the abovementioned models. This calculus is based on a clear distinction between values and computations, both at the level of types and terms, analogously to simply typed languages such as Levy's CallByPushValue and Egger et al.'s Enriched Effect Calculus. Compared to other dependently typed variants of CBPV in the literature, this calculus's distinctive feature is the computational sigmatype which provides a uniform treatment of typedependency in sequential composition. I will also show how to extend this calculus with algebraic effects and their handlers, with the latter being given a typebased treatment, internalising Plotkin and Pretnar's insight that handlers denote algebras (i.e., they ought to be computation types). I will also briefly show that in addition to their usual applications, handlers can also be used to reason about effects.