For straight-line code, something like %2 <- foo %0 %1 ... is effectively equivalent to (foo %0 %1 (lambda (%2) ...) Phis are sorta modele

For straight-line code, something like %2 <- foo %0 %1 ... is effectively equivalent to (foo %0 %1 (lambda (%2) ...) Phis are sorta modeled inversely: %1: %2 <- const 0 br %5 %3: %4 <- const 1 br %5 %5: %6 <- phi [%1 -> %2, %3 -> %4] ... becomes: (letrec ((%1 () (const 0 (lambda (%2) (%5 %2)))) (%3 () (const 1 (lambda (%4) (%5 %4)))) (%5 (%6) ...)) ...) The nice thing on paper about both of these is that you've broken every computation down into nice nameable bits; if you want to do some analysis (e.g. abstract interpretation) over the programs, you can store intermediate results as a map from names (like %4) to values. The traditional downside of CPS is that requiring lambdas be nested in order for things to be in scope can make some program transformations require "reshuffling" terms around in a way SSA doesn't require. The "cps soup" [0] approach used in Guile fixes this, but your terms look like they violate lexical scoping rules! [0]: https://wingolog.org/archives/2015/07/27/cps-soup https://wingolog.org/archives/2015/07/27/cps-soup