On the Proof Theory of Program Transformations
Martin C. Henson · Logic Journal of IGPL · 1995
We provide an intensional semantics for certain elementary program transformations by describing a translation from these transformations to the derivations of a simple theory of operations and types and we show that this semantics is intensionally faithful. Our objective is to understand precisely the ‘folk-lore’ view that program transformations are induction proofs in disguise and thus to understand more clearly the intensional (i.e. proof-theoretic) structure of a class of semi-formal program derivations.