Personal tools
You are here: Home Events LFCS seminar: Danel Ahman: A fibrational view on computational effects

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

— filed under: ,

What
  • LFCS Seminar
  • Upcoming events
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) category-theoretic viewpoint and from a lambda-calculus viewpoint.

First, I will show that similarly to the well-known 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; Eilenberg-Moore resolutions of split fibred monads; and the fibration of continuous families of cpos and liftings of CPO-enriched adjunctions.

From a lambda-calculus viewpoint, I will present a natural extension of vanilla Type Theory with computational effects that is sound and complete with respect to the above-mentioned 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 Call-By-Push-Value 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 sigma-type which provides a uniform treatment of type-dependency in sequential composition. I will also show how to extend this calculus with algebraic effects and their handlers, with the latter being given a type-based 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.

 

Document Actions