一句话：为 CBPV 识别交换转换，定义 CCNF 并给出基于 A-规范化的单遍翻译，用 join point 避免代码复制并证明求值等价。
本文研究 Levy 的 call-by-push-value（CBPV）语言中的交换转换（commuting conversions）。CBPV 通过区分值和计算并显式指定执行顺序，可同时包含 call-by-name 与 call-by-value，并适合作为编译器 IR；其替换求值语义支持组合式推理，βη-等价已用于证明编译器优化，但不能验证 A-规范化等编译 pass 所需的交换转换。作者识别出 CBPV 的交换转换，定义交换转换范式（CCNF），给出基于 A-规范化的单遍翻译，并借鉴 Maurer 等人的显式 join point 构造避免代码复制。作者证明良类型翻译后程序求值结果不变，所有结果在 Lean 4 中机器化验证。
Levy's call-by-push-value (CBPV) is a language that subsumes both call-by-name and call-by-value lambda calculi by syntactically distinguishing values from computations and explicitly specifying execution order. This low-level handling of computation suspension and resumption makes CBPV suitable as a compiler intermediate representation (IR), while its substitution evaluation semantics affords compositional reasoning about programs. In particular, βη -equivalences in CBPV have been used to justify compiler optimizations in low-level IRs. However, these equivalences do not validate commuting conversions , which are key transformations in compiler passes such as A-normalization. Such transformations syntactically rearrange computations without affecting evaluation order, and can reveal new opportunities for inlining. In this work, we identify the commuting conversions of CBPV, define a commuting conversion normal form (CCNF) for CBPV, present a single-pass transformation into CCNF based on A-normalization, and prove that well-typed, translated programs evaluate to the same result. To avoid the usual code duplication issues that also arise with A-normal form, we adapt the explicit join point constructs by Maurer et al. [2017] . Our results are all mechanized in Lean 4.
@article{paperbot3802,
title = {Commuting Conversions and Join Points for Call-by-Push-Value},
author = {Jonathan Chan and Madi Gudin and Annabel Levy and Stephanie Weirich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798210}
}