Program transformation and proof transformation

Abstract: "A 'linear-style' sequent calculus makes it possible to explore the close structural relationships between primitive recursive programs and their inductive termination proofs, and between program transformations and their corresponding proof transformations. In this context the recursive-to-tail-recursive transformation corresponds proof theoretically to a certain kind of cut elimination, called here 'call by value cut elimination'."