Algebraic effects, specification and refinement

Abstract

In the process of software engineering, we want to be sure that our code will function according to our requirements. The refinement calculus is a system that allows for mathematical correctness proofs, for imperative programs using a specific set of side effects. In the thesis, we explain how to use algebraic effects to add side effects to a purely functional program, and how to generalize concepts from the refinement calculus to develop and verify programs with algebraic effects. We work in the dependently typed programming language Agda, illustrating that this approach allows for formal verification of programs.