一句话：提出 ESL 规约逻辑，支持含命令式效应与高阶构造的零/单/多射效应处理器验证。
用户自定义效应与处理器常用于命令式效应，多射处理器还可支持非确定或概率程序中的回溯。现有验证工作受限：多射延续仅限纯设置、单射延续才可操作堆、或多射延续操作堆但帧规则受限。本文提出 Effectful Specification Logic（ESL），一种可支持无限制效应处理器的演算，使零射、单射、多射延续能与命令式效应及高阶构造共存。ESL 分阶段刻画行为，并为被调用效应、处理器与延续提供精确模型。作者实现了自动化验证原型，证明其可靠性，并通过案例研究与实验展示可行性。
Programming with user-defined effects and effect handlers has many practical use cases involving imperative effects. Additionally, it is natural and powerful to use multi-shot effect handlers for non-deterministic or probabilistic programs that allow backtracking to compute a comprehensive outcome. Existing works for verifying effect handlers are restricted in one of three ways: i) permitting multi-shot continuations under pure setting; ii) allowing heap manipulation for only one-shot continuations; or iii) allowing multi-shot continuations with heap-manipulation but under a restricted frame rule. This work proposes a novel calculus called Effectful Specification Logic (ESL) to support unrestricted effect handlers, where zero-/one-/multi-shot continuations can co-exist with imperative effects and higher-order constructs. ESL captures behaviors in stages, and provides precise models to support invoked effects, handlers and continuations. To show its feasibility, we prototype an automated verification system for this novel specification logic, prove its soundness, report on useful case studies, and present experimental results. With this proposal, we have provided an extended specification logic that is capable of modeling arbitrary imperative higher-order programs with algebraic effects and continuation-enabled handlers.
@article{SongFC24,
title = {Specification and Verification for Unrestricted Algebraic Effects and Handling},
author = {Yahui Song and Darius Foo and Wei-Ngan Chin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674656}
}