• Startseite
• Recherche
• Veröffentlichen
• Hilfe

Eingang zum Volltext

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:bsz:25-opus-5387
URL: http://www.freidok.uni-freiburg.de/volltexte/538/

Helsen, Simon

Region-based Program Specialization

Regionsbasierte Programmspezialisierung

Kurzfassung in Deutsch

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.