Håkon Robbestad Gylterud: The partiality monad and its algebras

In this talk I will give a description of the partiallity monad, its implementation in Martin-Löf type theory, and talk about my current research into its properties.

The partiality monad is an attempt to give an abstract descriptions of what a computation is, using categorical language. From any monad we can construct its Kleisli category, and in the case of the partiallity monad the Kleisli category models partial, computable functions.

I have begun an investigation into how this monad can be used to describe some aspects of computability in Martin-Löf type theory. I will relate this to other approaches to constructive computability theory (in particular Richman's "Church's thesis without tears"), and talk about the algebras for this monad and their connections to domain theory.