At the level of proofs (and the terms in Curry-Howard correspondence with them), the CPS translation turns the multiple-conclusion source derivations into single-conclusion LP derivations. The translation respects the invariant below. An active output formula A (marked off by the vertical bar in the box below) maps to a computation C(A), an active input formula to a continuation K(A). A cut then is interpreted as the application of C(A) to K(A).