Equality saturation : using equational reasoning to optimize imperative functions

Traditional optimizers have viewed imperative functions as a sequence or graph of commands. Some of these commands interact with the heap, throw exceptions, or interact with the outside world. Other commands simply read and modify local variables. In this dissertation, I take a different perspective on imperative functions. I view them as mathematical expressions, albeit with some quirks. These mathematical expressions have no need for local variables, making the flow of computation direct and so easier to reason about and manipulate. I will show how this enables equational techniques for program optimization, translation validation, and optimizer extensibilit