I have deposited my dissertation, "Polytypic Proving".

I am a member of the Cooperative Bug Isolation (CBI) group.

I was formerly a member of the Wisconsin Safety Analyzer (WiSA) group.

• Strengthening the inversion Tactic in Coq informal presentation Coq2010
• Effective Slicing: A Generalization of Full and Relevant Slicing technical report 2008
• Statistical Debugging Using Latent Topic Models ECML2007
• Proof Weaving WMM2006
• Tool Support for Proof Engineering UITP2006
• Gallimaufry: An Automated Framework for Proving Type Soundness CLASE2005

• Second Place in the PLDI 2008 ACM Student Research Competition (poster) (slides) (picture)

• Interactive, Scalable, Declarative Program Analysis: From Prototype to Implementation PPDP2007
• Statistical Debugging Using Compound Boolean Predicates ISSTA2007

• A proof of the decidablility of local closure. This proof is an extension of the libraries written to accompany Abstracting Syntax by Aydemir et al.
• A proof of type-soundness for a fragmentary language of references.