代数效应与处理器自动验证框架（扩展版）
计算机科学中的逻辑
2023-02-08 v3
摘要
代数效应与处理器是构建可恢复异常、轻量级线程、协程、生成器以及异步 I/O 等非局部控制流机制的强大抽象。所有这些特性都具有非常演进的语义，因此给演绎验证技术带来了非常有趣的挑战。事实上，针对包含这些构造的程序进行演绎验证的已有技术极少，而涉及自动化证明的则更少。在本文中，我们提出对 Cameleer（一个面向 OCaml 代码的演绎验证工具）的扩展，使得能够对代数效应与处理器进行推理。我们的方案利用异常来嵌入效应与处理器的行为，并采用去函数化来处理效应处理器所暴露的续延。
引用
@article{arxiv.2302.01265,
title = {A Framework for the Automated Verification of Algebraic Effects and Handlers (extended version)},
author = {Tiago Soares and Mário Pereira},
journal= {arXiv preprint arXiv:2302.01265},
year = {2023}
}