We present a new application of abstract interpretation to the formalization of source to source program transformations:
Abstract interpretation theory provides the ingredients for designing a syntactic source-to-source transformation as an abstraction of a semantics-to-semantics transformation, which correctness is formally established through an observational abstraction. In particular iterative transformation algorithms are abstraction of the fixpoint semantics of the subject program.
Several examples have been studied with this perspective such as blocking command elimination, program reduction, constant propagation, partial evaluation, etc.
\bibitem{Cousot01-ICLP} P.~Cousot. \newblock Design of Syntactic Program Transformations by Abstract Interpretation of Semantic Transformations (invited talk). \newblock In \emph{Proceedings of the 17th International Conference, ICLP 2001}, Ph{.} Codognet (Ed.), LNCS 2237, Paphos, Cyprus, November 26 -- December 1, 2001, pp. 4--5, Springer, Berlin, 2001. @inproceedings{Cousot01-ICLP, author = {Cousot, P{.}}, title = {Design of Syntactic Program Transformations by Abstract Interpretation of Semantic Transformations (invited talk)}, editor = {Codognet, Ph{.}}, pages = {4--5}, booktitle = {Proceedings of the Seventeenth International Conference, ICLP 2001}, address = {Paphos, Cyprus}, publisher = {LNCS 2237, Springer, Berlin}, month = {November/December}, year = 2001, }