一句话：将效应与余效应追踪引入 CBPV 类型系统，证明其可靠性并在 Coq 中机器化验证。
本文研究在 call-by-push-value（CBPV）类型系统中加入效应与余效应追踪。CBPV 因隔离效应并能清晰表达按名与按值计算而常用于编译。作者为 CBPV 设计带效应和余效应的类型系统，并证明 effect-and-coeffect soundness：类型可准确界定程序执行中触发的效应，并追踪程序对环境提出的需求。该可靠性对两种动态语义成立：一种通用语义可适配不同余效应；另一种面向资源使用，会丢弃未使用值和无纯计算，但保证有副作用的计算即使结果不被需要也始终求值。结果已在 Coq 中机器化验证。
Effect and coeffect tracking integrate many types of compile-time analysis, such as cost, liveness, or dataflow, directly into a language’s type system. In this paper, we investigate the addition of effect and coeffect tracking to the type system of call-by-push-value (CBPV), a computational model useful in compilation for its isolation of effects and for its ability to cleanly express both call-by-name and call-by-value computations. Our main result is effect-and-coeffect soundness , which asserts that the type system accurately bounds the effects that the program may trigger during execution and accurately tracks the demands that the program may make on its environment. This result holds for two different dynamic semantics: a generic one that can be adapted for different coeffects and one that is adapted for reasoning about resource usage. In particular, the second semantics discards the evaluation of unused values and pure computations while ensuring that effectful computations are always evaluated, even if their results are not required. Our results have been mechanized using the Coq proof assistant.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{TorczonAAVW24,
title = {Effects and Coeffects in Call-by-Push-Value},
author = {Cassia Torczon and Emmanuel Suárez Acevedo and Shubh Agrawal and Joey Velez-Ginorio and Stephanie Weirich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689750}
}