A Framework for the Automated Verification of Algebraic Effects and Handlers (extended version)

TL;DR

This paper introduces an extension to the Cameleer verification tool, enabling automated deductive verification of OCaml programs with algebraic effects and handlers by modeling their behavior through exceptions and defunctionalization.

Contribution

It presents a novel approach to verify algebraic effects and handlers in OCaml, addressing a gap in automated deductive verification techniques for such features.

Findings

Extended Cameleer to handle algebraic effects and handlers

Successfully modeled effects using exceptions and defunctionalization

Facilitated automated verification of complex control-flow features

Abstract

Algebraic effects and handlers are a powerful abstraction to build non-local control-flow mechanisms such as resumable exceptions, lightweight threads, co-routines, generators, and asynchronous I/O. All of such features have very evolved semantics, hence they pose very interesting challenges to deductive verification techniques. In fact, there are very few proposed techniques to deductively verify programs featuring these constructs, even fewer when it comes to automated proofs. In this paper, we present an extension to Cameleer, a deductive verification tool for OCaml code, that allows one to reason about algebraic effects and handlers. Our proposal embeds the behavior of effects and handlers using exceptions and employs defunctionalization to deal with continuations exposed by effect handlers.