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.