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

[Code]

Static analysis on incomplete programs is hard. I worked with David Van Horn towards remedying this by mechanizing a refinement relation soundness proof over modular black hole semantics.

Abstract Interpretation of Android Apps

[Code]

What security properties can we statically guarantee about Android Apps? As a part of the U-Combinator group, I applied theoretical results in abstract interpretation to the Android stack. More details can be found in this pdf abstract.

Undergraduate Thesis

[PDF] | [Blog]

A study into the Curry-Howard Isomorphism.

Primality Testing

[Code] | [PDF]

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.

Python Compiler

[Code]

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.

crowdLabs

[PDF] | [Site]

crowdLabs is a social visualization repository for the scientific workflow management system VisTrails. It adopts the model used by social Web sites and that integrates a set of usable tools and a scalable infrastructure to provide an environment for scientists to collaboratively analyze and visualize data.

VisTrails

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.