Reference. Commuting Conversions and Join Points for Call-by-Push-Value

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.

Cite

Cite as @chan-2026-commuting (helia, typst) · \cite{chan-2026-commuting} (LaTeX)
BibTeX
bibtex · 1 line
@article{chan-2026-commuting, title={Commuting Conversions and Join Points for Call-by-Push-Value}, volume={10}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3798210}, DOI={10.1145/3798210}, number={OOPSLA1}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Chan, Jonathan and Gudin, Madi and Levy, Annabel and Weirich, Stephanie}, year={2026}, month=Apr, pages={289–313} }
hayagriva YAML (typst)
yaml · 20 lines
chan-2026-commuting:
  type: article
  title: Commuting Conversions and Join Points for Call-by-Push-Value
  author:
  - Chan, Jonathan
  - Gudin, Madi
  - Levy, Annabel
  - Weirich, Stephanie
  date: 2026-04
  page-range: 289-313
  url: http://dx.doi.org/10.1145/3798210
  serial-number:
    doi: 10.1145/3798210
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: OOPSLA1
    volume: 10
chan-2026-commuting reference entries/refs/chan-2026-commuting/chan-2026-commuting.hel