The formal relationship between direct and continuation-passing style optimizing compilers: A synthesis of two paradigms

Compilers for higher-order programming languages like Scheme, ML, and Lisp can be broadly characterized as either "direct compilers" or "continuation-passing style (CPS) compilers", depending on their main intermediate representation. Our central result is a precise correspondence between the two compilation strategies. Starting from the theoretical foundations of direct and CPS compilers, we develop relationships between the main components of each compilation strategy: generation of the intermediate representation, simplification of the intermediate representation, code generation, and data flow analysis. For each component, our results pinpoint the superior compilation strategy, the reason for which it dominates the other strategy, and ways to improve the inferior strategy. Furthermore, our work suggests a synthesis of the direct and CPS compilation strategies that combines the best aspects of each. The contributions of this thesis include a comprehensive analysis of the properties of the CPS intermediate representation, a new optimal CPS transformation and its inverse, a new intermediate representation for direct compilers, an equivalence between the canonical equational theories for reasoning about continuations and general computational effects, a sound and complete equational axiomatization of the semantics of call-by-value control operators, a methodology for deriving equational logics for imperative languages, and formal relationships between code generators and data flow analyzers for direct and CPS compilers. These contributions unify concepts in two distinct compilation strategies, and can be used to compare specific compilers