Certification of programs with computational effects

TL;DR

This paper develops formal methods and Coq libraries for verifying program properties involving various computational effects such as states, exceptions, and non-termination, bridging functional and non-functional programming paradigms.

Contribution

It introduces a formal framework using decorated logic for reasoning about effects and implements Coq tools to verify properties across multiple effects.

Findings

Formalized decorated logic for effects

Developed Coq libraries for effect verification

Enabled combined effects reasoning

Abstract

In purely functional programming languages imperative features, more generally computational effects are prohibited. However, non-functional lan- guages do involve effects. The theory of decorated logic provides a rigorous for- malism (with a refinement in operation signatures) for proving program properties with respect to computational effects. The aim of this thesis is to first develop Coq libraries and tools for verifying program properties in decorated settings as- sociated with several effects: states, local state, exceptions, non-termination, etc. Then, these tools will be combined to deal with several effects.