Combining effects and coeffects via grading

What is it about?

This paper presents a new model of computation that can be used for reasoning about the correctness of programs and various properties of those programs. The model takes the form of a simple programming language (a calculus) with a set of logical rules constraining which programs are valid. These logical rules also provide additional information about the program under study. The calculus brings together two threads of existing research on "coeffects" and "effects"-- two kinds of program behaviour. The model is notable in that in provides a framework for combining both coeffects and effects together, allowing for a whole new kind of fine-grained program reasoning.

Featured Image