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

<jats:p> <jats:xref ref-type="bibr">Levy's</jats:xref> 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, <jats:italic toggle="yes">βη</jats:italic> -equivalences in CBPV have been used to justify compiler optimizations in low-level IRs. However, these equivalences do not validate <jats:italic toggle="yes">commuting conversions</jats:italic> , 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. </jats:p> <jats:p> In this work, we identify the commuting conversions of CBPV, define a <jats:italic toggle="yes">commuting conversion normal form</jats:italic> (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 <jats:xref ref-type="bibr">Maurer et al. [2017]</jats:xref> . Our results are all mechanized in Lean 4. </jats:p>

@article{chan2026,
  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},
  issue = {OOPSLA1},
  year = 2026,
  month = 4,
  day = 10,
  doi = {10.1145/3798210},
}