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 outline some of the currently available techniques for the verification of programs with algebraic effects. We then build off them to create a mostly automated verification framework by extending Cameleer, a tool which verifies OCaml code using GOSPEL and Why3. This framework embeds the behavior of effects and handlers using exceptions and defunctionalized functions.

翻译：代数效应与句柄是一种强大的抽象机制，可用于构建非局部控制流结构，如可恢复异常、轻量级线程、协程、生成器及异步I/O。此类特性均具有高度演进的语义，因而为演绎验证技术带来极具挑战性的问题。事实上，目前针对包含这些构造的程序进行演绎验证的技术极少，而实现自动化证明的方法更是凤毛麟角。本文概述了当前可用的若干代数效应程序验证技术，并在此基础上通过扩展Cameleer（一款基于GOSPEL和Why3验证OCaml代码的工具），构建了一个高度自动化的验证框架。该框架利用异常与去函数化函数来嵌入效应与句柄的行为。