I work in the Programming Systems group under Sorin Lerner and Ranjit Jhala. In my research, I design and build tools that help ensure software correctness. To prove programs are error free, I've used proof assistants, SMT solvers, translation validation, and type systems.
My projects include:
| XCERT | Brings extensibility to verified compilers |
| PEC | Automates correctness proofs for compiler optimizations |
| EQSAT | Attacks phase ordering and extends to translation validation |
| DTAR | Statically checks Java / Database interactions |
| PLDI 10 | Bringing Extensibility to Verified Compilers |
| Zachary Tatlock, Sorin Lerner | |
| talk slides bib | |
| PLDI 09 | Proving Optimizations Correct using Parameterized Program Equivalence |
| Sudipta Kundu, Zachary Tatlock, Sorin Lerner | |
| talk slides bib | |
| POPL 09 | Equality Saturation: A New Approach to Optimization |
| Ross Tate, Mike Stepp, Zachary Tatlock, Sorin Lerner | |
| talk * slides * bib | |
| OOPSLA 08 | Deep Typechecking and Refactoring |
| Zachary Tatlock, Chris Tucker, David Shuffleton, Ranjit Jhala, Sorin Lerner | |
| slides bib |
My research interests cover compilers, program analysis, and formal methods. Even outside of research, I love programming and try to code for fun every day. When not hacking, I'm cycling around San Diego, playing ultimate frisbee, or enjoying board games with friends.
I graduated from Purdue University in Spring 2007 with degrees in Computer Science and Mathematics. As an undergraduate, I was fortunate to perform research with Suresh Jagannathan on the SML compiler MLton. For my Honors Project, advised by Antony Hosking, I designed and implemented a domain specific language to control a giant neon sculpture over the web. Over nearly three years, I ran the lab component of Purdue's introductory Java programming class, CS 180.