log in  |  register  |  feedback?  |  help  |  web accessibility
PhD Proposal: Higher-order Flow Analysis, Types, and Program Optimization
Benjamin Quiring
Tuesday, May 6, 2025, 9:00-11:00 am
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

Program analysis is used to determine semantic facts about programs in order to optimize or verify them. Analyses for functional languages, or more precisely languages with higher-order functions, are more complex to define due to control-flow being intertwined with data-flow. These analyses are often difficult to implement efficiently and correctly. We present a program analysis for typed higher-order programming languages that is easy to understand, efficient, precise, and extensible. It is easy to implement and maintain, as it extends existing type inference procedures in a simple-manner.

The results of flow analysis are used to guide flow-directed optimizations, which are non-local, interprocedural transformations to programs that change the representation and interface of values, especially functions. We describe how to formulate these transformation based on the results of any analysis. For the particular case of our analyses, they come with the added benefit of preserving the typed behavior of the term.

Finally, we present plans to verify such program optimizations using a general framework that is easily extended by optimization designers. We additionally present extensions of the analysis towards more complicated source languages, along with a technique to make the analysis responsive to program updates, whether due to programmer updates or compiler transformations.

Bio

Benjamin Quiring is a fourth year PhD student studying under David Van Horn. His research interests lie in the intersection of analysis and optimization of functional programming languages, analysis and internal representation design, verification.

This talk is organized by Migo Gui