P. Cousot, Design of Syntactic Program Transformations by Abstract Interpretation of Semantic Transformations

Patrick Cousot.
Design of Syntactic Program Transformations by Abstract Interpretation of Semantic Transformations (invited talk).
In Proceedings of the 17th International Conference, ICLP 2001, Philippe Codognet (Ed.), Lecture Notes in Computer Science 2237, Paphos, Cyprus, November 26 -- December 1, 2001, pp. 4—5, © Springer.
Paper: PDF (58.4 KB)
Abstract: Traditionally, static program analysis has been used for offline program transformation i.e. an abstraction of the subject program semantics is used to determine which syntactic transformations are applicable. A classical example is binding-time analysis before partial evaluation.
We present a new application of abstract interpretation to the formalization of source to source program transformations:
- The semantic transformation is understood as an abstraction of the subject program semantics. The intuition is that the transformed semantics is an approximation of the subject semantics because, most often, redundant elements of the subject semantics have been eliminated;
- The correctness of the semantic transformation is expressed by an observational abstraction. The intuition is that the subject and transformed semantics should be exactly the same when abstracting away from irrelevant hence unobserved details;
- Finally, the syntax of a program is shown to be an abstraction of its semantics (in that details of the execution are lost) so that the transformed program is an abstraction of the transformed semantics.
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.
See also the full paper.
Slides of the 75mn ICLP'01 presentation are available in v 4 slides per A4 landscape sheet format .pdf.gz (536.8 KB).

\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,
}