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 代码的一种推算性核查工具,它使人们能够解释代数效应和处理者。我们的建议包含了使用例外处理法的效果和操作者的行为,并采用不起作用的方法处理由效果处理者暴露的连续问题。