Abstract

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 structure of a class of semi-formal program derivations