Equivalence-Preserving Closure Conversion in the Presence of Mutable References
Closure conversion is a compiler pass that hoists free variables out of functions and into environments, simplifying subsequent passes. In “Verifying an Open Compiler Using Multi-Language Semantics” Perconti and Ahmed show a typed closure conversion pass semantics-preserving for a language with recursion. My current work attempts to determine if this compiler pass preserves not only semantics but also equivalences, when the language is extended with mutable references.
Equivalence-Preserving CPS Translation with recursive types
In “An Equivalence-Preserving CPS Translation via Multi-Language Semantics” Ahmed and Blume claim their approach scales to languages with recursive types. During the first year of my PhD I attempted, and failed, to realize this claim. More details on the intricacies of this extension can be found in our HOPE 13 abstract.
Black Hole Analysis
Abstract Interpretation of Android Apps
U-Combinator group, I applied theoretical results in abstract interpretation to the Android stack. More details can be found in this pdf abstract.
For Suresh Venkat's graduate level Algorithms course our group implemented ECPP and AKS primality testing algorithms. Furthermore we hybridized the two algorithms as described by Cheng. This involves doing one round of ECPP to reduce the prime to be proved by AKS.
I wrote a compiler for a subset of Python3 in Haskell for Matt Might's Compilers. The lexer and parser were built using derivative methods. The parsed result was a high intermediate language which was then transformed into a low intermediate language and put into Continuation Passing Style. I then translated the CPS representation into a strict subset of C which was compiled down to x86 using GCC.
VisTrails is an open-source scientific workflow and provenance management system developed at the University of Utah that provides support for data exploration and visualization. A key distinguishing feature of VisTrails is a comprehensive provenance infrastructure that maintains detailed history information about the steps followed and data derived in the course of an exploratory task: VisTrails maintains provenance of data products, of the workflows that derive these products and their executions.