# Danel Ahman: A fibrational view on computational effects

**Abstract:** In this talk, I will give an overview of my work on the interplay between dependent types and computational effects. In particular, I
will discuss the syntax and semantics of a dependently typed lambda
calculus with computational effects based on a clear distinction
between values and computations akin to Call-By-Push-Value and the
Enriched Effect Calculus. The distinctive feature of this calculus is
the computational sigma-type, which provides a uniform treatment of
type-dependency in sequential composition, and which can also be used
to give semantics to the effect system of the Idris language. In the
talk, I will also discuss how one can extend this calculus with
algebraic effects and their handlers, and show that in addition to
being a convenient programming abstraction, the latter also provide
a useful mechanism for reasoning about effectful computations.

The fibrational semantics of this calculus demonstrates that similarly to well-known results from the simply typed setting, it is also natural to model computational effects in the dependently typed setting using monads and adjunctions. 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 the Enriched Effect Calculus; Eilenberg-Moore resolutions of split fibred monads; and the fibration of continuous families of cpos and liftings of CPO-enriched adjunctions, so as to model general recursion.