Environment Analysis of Higher-Order Languages

Show full item record

Please use this identifier to cite or link to this item: http://hdl.handle.net/1853/16289

Title: Environment Analysis of Higher-Order Languages
Author: Might, Matthew Brendon
Abstract: Any analysis of higher-order languages must grapple with the tri-facetted nature of lambda. In one construct, the fundamental control, environment and data structures of a language meet and intertwine. With the control facet tamed nearly two decades ago, this work brings the environment facet to heel, defining the environment problem and developing its solution: environment analysis. Environment analysis allows a compiler to reason about the equivalence of environments, i.e., name-to-value mappings, that arise during a program's execution. In this dissertation, two different techniques-abstract counting and abstract frame strings-make this possible. A third technique, abstract garbage collection, makes both of these techniques more precise and, counter to intuition, often faster as well. An array of optimizations and even deeper analyses which depend upon environment analysis provide motivation for this work. In an abstract interpretation, a single abstract entity represents a set of concrete entities. When the entities under scrutiny are bindings-single name-to-value mappings, the atoms of environment-then determining when the equality of two abstract bindings infers the equality of their concrete counterparts is the crux of environment analysis. Abstract counting does this by tracking the size of represented sets, looking for singletons, in order to apply the following principle: If {x} = {y}, then x = y. Abstract frame strings enable environmental reasoning by statically tracking the possible stack change between the births of two environments; when this change is effectively empty, the environments are equivalent. Abstract garbage collection improves precision by intermittently removing unreachable environment structure during abstract interpretation.
Type: Dissertation
URI: http://hdl.handle.net/1853/16289
Date: 2007-06-29
Publisher: Georgia Institute of Technology
Subject: Static analysis
Lambda calculus
Programming languages
Data structures (Computer science)
Abstract data types (Computer science)
Computer programs Verification
Department: Computing
Advisor: Committee Chair: Olin Shivers; Committee Member: Mitchell Wand; Committee Member: Panagiotis Manolios; Committee Member: Santosh Pande; Committee Member: Yannis Smaragdakis
Degree: Ph.D.

All materials in SMARTech are protected under U.S. Copyright Law and all rights are reserved, unless otherwise specifically indicated on or in the materials.

Files in this item

Files Size Format View
might_matthew_b_200708_phd.pdf 867.4Kb PDF View/ Open

This item appears in the following Collection(s)

Show full item record