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.

翻译：代数效应与处理器是一种强大的抽象机制，可用于构建非局部的控制流结构，例如可恢复异常、轻量级线程、协程、生成器以及异步I/O。所有这些特性都具有高度演化的语义，因此对演绎验证技术提出了极具挑战性的难题。事实上，目前仅有极少数研究提出通过演绎方式验证包含这些构造的程序，而涉及自动化证明的方案更是凤毛麟角。本文提出了一种针对Cameleer（OCaml代码的演绎验证工具）的扩展方案，使其能够推理代数效应与处理器。我们的方案通过异常来嵌入效应和处理器的行为，并采用去函数化技术处理效应处理器暴露的续延。