Handling Side-Effects using Resource Dependent Algebraic Effects

I am giving a talk today about some work on reasoning about program side effects in Idris.

The abstract is:

Dependent types provide an expressive environment in which one can specify, and reason about, the properties of our software programs.

In this talk I will introduce dependent types and examine how we can reason about program behaviour using finite state machines and type-level modelling.

Slides are not available.