Accepted for presentation at the 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003), ENTCS series, Volume 82.2, Elsevier Science, 2004.
Abstract
The static single assignment (SSA) form is central to a range of
optimisation algorithms relying on data flow information, and hence, to
the correctness of compilers employing those algorithms. It is well known
that the SSA form is closely related to lambda terms (i.e., functional
programs), and, considering the large amount of energy expended on
theories and frameworks for formal reasoning in the lambda calculus, it
seems only natural to leverage this connection to improve our capabilities
to reason about compiler optimisations. In this paper, we discuss a new
formalisation of the mapping from SSA programs to a restricted form of
lambda terms, called administrative normal form (ANF). We
conjecture that this connection improves our ability to reason about
SSA-based optimisation algorithms and provide a first data point by
presenting an ANF variant of a well known SSA-based conditional constant
propagation algorithm.
Published version in PostScript or PDF [direct from Elsevier]
PostScript (preprint) (15 pages)
This page is part of Manuel Chakravarty's WWW-stuff.