Program certification with computational effects

TL;DR

This paper introduces a proof system for exceptions in programming languages, extending Moggi's monad approach, and combines it with a dual proof system for state effects, all implemented in Coq.

Contribution

It presents a novel proof system for exceptions, extends Moggi's monad framework, and integrates it with a dual system for state effects within Coq.

Findings

Proof system for exceptions involving raising and handling

Duality between exception and state effect proof systems

Implementation of combined effect systems in Coq

Abstract

Dynamic evaluation is a paradigm in computer algebra which was introduced for computing with algebraic numbers. In linear algebra, for instance, dynamic evaluation can be used to apply programs which have been written for matrices with coefficients modulo some prime number to matrices with coefficients modulo some composite number. A way to implement dynamic evaluation in modern computing languages is to use the exceptions mechanism provided by the language. In this paper, we pesent a proof system for exceptions which involves both raising and handling, by extending Moggi's approach based on monads. Moreover, the core part of this proof system is dual to a proof system for the state effect in imperative languages, which relies on the categorical notion of comonad. Both proof systems are implemented in the Coq proof assistant, and they are combined in order to deal with both effects at the same time.