Accepted for presentation at the 2nd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2003), ENTCS series, Volume 82.2, Elsevier Science, 2004.
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.