Proving and applying program transformations expressed with second-order patterns

Summary We propose a program transformation method based on rewriting-rules composed of second-order schemas. A complete second-order matching algorithm is presented that allows effective use of these rules. We show how to formally prove the correctness of the rules using a denotational semantics for the programming language. We establish the correctness of the transformation method itself, and give techniques pertaining to its actual implementation. The paper is illustrated with recursion removal examples.A preliminary version of this paper appeared in the Proceedings of the International School of Theory and Application of Computers, ERICE (Sicily), May 1976