{"id":{"repo_id":"freiburg-diss","oai_identifier":"oai:freidok.uni-freiburg.de:538"},"canonical_url":"https://search.dev.ndltd.org/etd/freiburg-diss/oai:freidok.uni-freiburg.de:538","repository":{"repo_id":"freiburg-diss","name":"University of Freiburg","base_url":"https://freidok.uni-freiburg.de/oai/oai2.php"},"display":{"title":"Region-based Program Specialization","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Helsen, Simon"],"institution":null,"degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Thiemann, Peter"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":null,"date_issued":"","date_published":null,"updated_at":"2026-07-24T02:21:46Z","subjects":["Region Calculus","Partial Evaluation","Operational Semantics","Program Semantics","Program Optimization"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://freidok.uni-freiburg.de/data/538","outbound_label":"Repository record","outbound_source":"source_url"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Thiemann, Peter"]},{"key":"dc:creator","label":"Author","values":["Helsen, Simon"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:type","label":"Dc Type","values":["DoctoralThesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Region Calculus","Partial Evaluation","Operational Semantics","Program Semantics","Program Optimization"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Region-based Program Specialization","Regionsbasierte Programmspezialisierung"]}]}],"canonical_facts":{"dc:contributor":["Thiemann, Peter"],"dc:creator":["Helsen, Simon"],"dc:description.abstract":["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."],"dc:format.medium":["application/pdf"],"dc:subject":["Region Calculus","Partial Evaluation","Operational Semantics","Program Semantics","Program Optimization"],"dc:title":["Region-based Program Specialization","Regionsbasierte Programmspezialisierung"],"dc:type":["DoctoralThesis"]},"updated_at":"2026-07-24T02:21:46Z"}