Region-based Program Specialization

Program specialization or partial evaluation is a proven program optimization technique dating back to the early seventies. One common flavor of program specialization is offline partial evaluation. It employs a program analysis to determine what operations can be reduced at specialization time. Historically, offline systems used simple binding-time annotation techniques, or considered simply-typed programming languages. These approaches have hampered offline methods in reaching their full potential. In this thesis, we aim to address these limitations. We describe the development of a new and entirely operational theory for offline polymorphic specialization of ML-like languages by combining techniques from dynamic memory management with program specialization. Our approach is based on the region calculus of Tofte and Talpin, a polymorphically typed lambda calculus with annotations that make memory allocation and deallocation explicit. The formal correctness proof of our novel specialization technique based on a region type system requires two theoretical building blocks: a type soundness proof for the region calculus and a correctly proven equational theory between region-annotated terms. Putting these together yields a new method for offline partial evaluation of functional programming languages with an ML-style typing discipline. Our method comprises a polymorphic binding-time analysis with polymorphic recursion, which is conceived as a constraint analysis on top of region inference. The relation between program specialization and regions is a result of regarding binding times as properties of regions.

Author dc:creator

• Helsen, Simon

Contributors dc:contributor

• Thiemann, Peter

• Region Calculus
• Partial Evaluation
• Operational Semantics
• Program Semantics
• Program Optimization

Repository record source_url

https://freidok.uni-freiburg.de/data/538

OAI identifier oai:identifier

oai:freidok.uni-freiburg.de:538