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
Cites 18 works (1 here)
With notes (1)
Call-By-Push-Value: A Functional/Imperative Synthesis levy-2003-callbypushvalue
External (17)
- Artifact for "Commuting Conversions and Join Points for Call-By-Push-Value" (2026)
- A Verified Cost Model for Call-By-Push-Value (2025)
- zydeco-lang/zydeco: v0.2.2 (software) (2025)
- A Low-Level Look at A-Normal Form (2024)
- Closure Conversion in Little Pieces (2023)
- Compiling with Call-by-push-value (CALCO 2023 presentation) (2023)
- Compiling with continuations, or without? whatever (2019)
- Call-by-push-value in Coq: operational, equational, and denotational theory (2019)
- From Call-by-push-value to Stack-Based TAL? (LOLA 2019 presentation) (2019)
- Structural Operational Semantics for Control Flow Graph Machines (2018)
- A Formal Equational Theory for Call-By-Push-Value (2018)
- Compiling without continuations (2017)
- The Lean Theorem Prover (System Description) (2015)
- Compiling with continuations, continued (2007)
- Stack-based typed assembly language (2002)
- The essence of compiling with continuations (1993)
- Notions of computation and monads (1991)