Papers
[2008]
SASyLF: An Educational Proof Assistant for Language Theory
With Jonathan Aldritch and Key Shin. Accepted to FDPE 2008, September 21, 2008.Linear Logical Algorithms
With Frank Pfenning. Presented at ICALP 2008, July 6-13, 2008. [more]Proofs From Tests
With Nels Beckman, Aditya Nori, and Sriram K. Rajamini. Accepted to ISSTA 2008, July 20, 2008. [ACM link][MSR Tech Report][1982-2007]
Mechanized Metatheory for User-Defined Type Extensions
With Daniel Marino, Brian Chin, Todd Millstein, Gang Tan, and David Walker. Presented at the ACM SIGPLAN Workshop on Mechanizing Metatheory, September 21, 2006. [PDF][BibTeX]Twelf as a unified framework for language formalization and implementation
Advised by David Walker. Princeton University undergraduate senior thesis 18679, April 29, 2005. [PDF] [Associated code][BibTeX]Talks
Concurrent Algorithms in Linear Logic Programming
At the informal "New Programming Models and Tools for Concurrency" workshop, Carnegie Mellon, February 14, 2008. A slightly different perspective on the material in "Linear Logical Algorithms." [PDF]The LF Logical Framework (part 1 of 2)
At Microsoft Research, India, August 3, 2007. [PDF, Flash of Keynote talk]The Twelf Metalogical Framework (part 2 of 2)
At Microsoft Research, India, August 13, 2007. [PDF, Flash of Keynote talk]More information can be found on the Twelf Wiki