一句话：提出深度效应处理器细粒度归约理论，给出标准归约策略，证明其保持观测等价，并用于重写优化与NBE规范化。
效应处理器是函数式语言中组织计算效应的流行机制。其传统操作语义适合实现，却不适合作为归约/重写理论。本文受 shift0 的归约理论启发，为深度效应处理器提出一种细粒度归约理论，并给出标准归约策略。作者通过模拟论证将该策略与传统非局部操作语义相联系，证明该归约理论保持相对于经典处理器语义的观测等价，因而可作为带处理器语言的重写理论；该重写系统与已有基于类型的优化基本一致。文中还证明了合流性与标准化定理，并给出首个面向效应处理器的 normalization-by-evaluation 算法，证明其可靠性与完备性，同时确立了 lift 算子不能由其他构造表达。
Effect handlers are a modern and increasingly popular approach to structuring computational effects in functional programming languages. However, while their traditional operational semantics is well-suited to implementation tasks, it is less ideal as a reduction theory. We therefore introduce a fine-grained reduction theory for deep effect handlers, inspired by our existing reduction theory for shift0, along with a standard reduction strategy. We relate this strategy to the traditional, non-local operational semantics via a simulation argument, and show that the reduction theory preserves observational equivalence with respect to the classical semantics of handlers, thus allowing its use as a rewriting theory for handler-equipped programming languages -- this rewriting system mostly coincides with previously studied type-based optimisations. In the process, we establish theoretical properties of our reduction theory, including confluence and standardisation theorems, adapting and extending existing techniques. Finally, we demonstrate the utility of our semantics by providing the first normalisation-by-evaluation algorithm for effect handlers, and prove its soundness and completeness. Additionally, we establish non-expressibility of the lift operator, found in some effect-handler calculi, by the other constructs.
@article{paperbot1922,
title = {A General Fine-Grained Reduction Theory for Effect Handlers},
author = {Filip Sieczkowski and Mateusz Pyzik and Dariusz Biernacki},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607848}
}