Awards
Talks
POPL 2009
Publications
The links below contain more than the usual pdf files. They also contain an embedded video of the presentation and the powerpoint slides, for those people who would like a quick overview before reading the paper. They also have answers to common questions we have recieved.
- Generating Compiler Optimizations from Proofs (POPL 2010)
with Michael Stepp and Sorin Lerner - Equality Saturation: A New Approach to Optimization (POPL 2009)
with Michael Stepp, Zachary Tatlock, and Sorin Lerner
Active Projects
Below are the projects I am currently working on. There are many others I hope to work on once I have the time. I think my plate's pretty full at the moment.
- Equality-Based Applications: I am working with Sorin Lerner, Michael Stepp and Zachary Tatlock on continuing our research with Equality Saturation. We have found many avenues to explore, some our own and some suggested by other researchers in the community. Most recently we applied our proof generalization techniques to equality saturation in order to learn optimizations from concrete code transformations which can even be supplied by the programmer.
- Applications of Proof Generalization: In the above optimization learning project, proofs play a key role in our algorithm. In fact, we developed an abstract algorithm for generalizing proofs. When applied to proofs of program equivalence, these generalizations produce program optimizations. However, our abstract algorithm is expressed categorically, so it can be applied to many domains besides our own. We have already found applications to database query optimization, type debugging in Hindley-Milner-based languages, contract debugging, and type generalization. I hope to make this framework accessible to other researchers so that they may exploit our algorithm to solve their own problems, in the same way abstract interpretation has been a useful algorithm framework for program analyses.
- Integrating Effects into Language Design: I am working with Daan Leijen on incorporating monadic effects into the design of functional languages. This has been an interesting exploration into the design and implementation philosophies of the various functional languages already out there. Some of these philosophies, such as type inference, we are keeping and even embellishing upon, while other philosophies, such as currying, we are discarding because they interact poorly with effects. In the future, I hope to do the same investigation into imperative languages and examine which design philosophies mix well with effectful programming.
- Type Inference for Assembly Code from Object-Oriented Programs: I am working with Juan Chen and Chris Hawblitzel on inferring types for typed assembly language designed specifically for object-oriented programs. We have promising findings and are working on a compiler plugin which requires almost no changes to the compilation process.
- Existential Types: In the above type inference project, existential types play a critical role. Existential types can be quite challenging to work with when the standard pack and open operations are made implicit, and joining these types is a fundamental component of our type inference. Interestingly, I found a very general solution using category theory of all things. This general solution dramatically simplified designing our type system since we could know which changes would or would not break joins. Changes like adding generics turn out to be not a problem, while changes like null pointers have to be done carefully otherwise joins do not exist. We have submitted our framework to ECOOP '09. I am also looking into other applications of existential types made possible by this framework.
Research Interests
I am a fan of programming languages, or really programming language design. After my work in compiler optimizations, I have realized a strong need for making the intended and expected meaning of a program more explicit in the language, both for the programmer's sake and the compiler's sake. I am looking into how to design languages so that this information is available to both the programmer and compiler without being a burder to either. More casually, I also enjoy bits of linguisitcs and hope to incorporate it into language design. Having been a math major in my dark past, I have taken a fondness to category theory, which has already heavily influenced my research and will likely influence future language designs of mine. Ironically, my most recent application of category theory was to assembly code. I love how something so abstract can greatly contribute to something so concrete.
Research Internships
I interned under Daan Leijen at Microsoft Research in Redmond in Summer/Fall 2009. We designed a pure but effectful functional programming language, as well as a Hindley-Milner-like type inference algorithm with effects and higher-order polymorphism (based on Daan's HMF). In doing so, I improved compiler technology for inferring higher-ranked polymorphism. I also managed to generalize monads in order to formalize effect systems with multiple interacting effects. We are pursuing publications on these research topics.
I interned under Juan Chen and Chris Hawblitzel at Microsoft Research in Redmond in Summer/Fall 2008. I designed a type inference algorithm for an x86 assembly type system for object-oriented programs. In doing so I designed a framework for existential types based on category theory, which has proven to be intuitive, powerful, and flexible. We are pursuing publications on both research topics.
Internships
I have interned at Treyarch, a sub-division of Activision, twice now. The first time I worked on the early stages of the Spider-Man 3 console game. The second time I worked on Spider-Man: Web of Shadows. My biggest contributions have been in improving the scripting language used by the game designers, and this may have somewhat fostered my enjoyment of programming languages. I have also worked a lot with computational geometry and corresponding graph theory.
Before that, I interned at CustomFlix. At the time, CustomFlix was a very small internet company which processed, distributed, and marketed personal videos. I held various roles such as architect, tester, lead, and web-developer.
Post-Script
I stole this page from Patrick "Maxim" Rondon.
I found my grandpa online. Thought it was pretty cool.