Skip to main content
Open Access Publications from the University of California

UC San Diego

UC San Diego Electronic Theses and Dissertations bannerUC San Diego

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 extensibility

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View