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代码），构建了一个近乎全自动化的验证框架。该框架利用异常和去函数化函数来嵌入效应与处理器的行为。