Algebraic Effects and Guarded Recursion

Dependently typed programming languages allow for specifications of programs to be expressed in types and proofs to be machine verified. This can be used for formal verification of software, but unfortunately the logical interpretation of type theory forces restrictions on type theory as a programming language. In recent work we have shown how recursion can be added safely to type theory without breaking the logical interpretation, and a version of this has been implemented in Agda.

This project looks at how to combine guarded recursion with algebraic effects, i.e., actions such as exception raising, access to memory and probabilistic choice. This will allow the programmer to write recursive programs using these effects. We do this by studying how to combine the algebraic theories for these effects with the steps of guarded recursion, and describing the monads they give rise to. We focus on two applications: Advanced notions of store and probabilistic choice.