At the level of proofs, given the above interpretation of types, the task is to find an LP proof for the sequent below, the image of the \ and / elimination rules for A, A\B ⊢ B and B/A, A ⊢ B. Whereas in the source calculus there is only one way of putting together an A\B (or B/A) function with its A argument, in the target calculus there is a choice as to the evaluation order: do we want to first evaluate the translation image of the argument, then that of the function, or the other way around.  We write ·v for the first option (call-by-value) and ·n for the second (call-by-name).  In the target language, m and n are variables of type A′ → B′ and A′ respectively; k is the resulting B′ → t continuation.