Dissertation

• The Logical Basis of Evaluation Order and Pattern-Matching. Defended April 17, 2009. [defense slides]

Journal articles

• On the unity of duality. Annals of Pure and Applied Logic 153:1 (2008), special issue on "Classical logic and computation". [doi]

Conference and workshop papers and talks

• Defunctionalizing focusing proofs. [twelf] [more twelf] Presented at PSTT 09.
• Refinement types and computational duality. Presented at PLPV 09.
• Duality and polarity in type theory. Talk, May 23, 2008 at MFPS 08.
• Polarity and duality in type theory. Talk, February 20, 2008 at DTP 08.
• Focusing on binding and computation. With Dan Licata and Bob Harper. Presented at LICS 08. [tech report]
• Focusing and higher-order abstract syntax. Presented at POPL 08. [coq] [errata]

Other talks

• Walking the way of duality. Talk, October 10, 2008 at the SCS Student Seminar Series.
• From AHOS to HOAS. March 4, 2008 at the INRIA Rocquencourt Gallium-Moscova Seminar. [abstract]
• Focusing with higher-order rules. Talk, February 28, 2008 at the LIX Comète-Parsifal Seminar. [abstract]
• Focusing proofs and the Curry-Howard correspondence. February 26, 2008 at the PPS Semantics and Realizability Seminar. [abstract]
• Proof counts. Talk, November 3, 2005 at the Rutgers Experimental Mathematics Seminar. [ps]

Et cetera

• Soundness of labelled deduction. August, 2005. An attempt at a constructive proof of the soundness of labelled deduction for intuitionistic logic. This is essentially a variation on the usual "prime context" approach establishing completeness of intuitionistic logic with respect to Kripke semantics. For a more novel approach, see Jason Reed and Frank Pfenning's "Intuitionistic letcc via labelled deduction".
• Modal BI and Separation Logic. June, 2005. Describes how to extend the logic of bunched implications with an S4-like box modality, and its relationship to "purity" in separation logic.
• Nathack: a natural language interface for nethack. January, 2003. With Cassia Martin, David Molnar, and Dev Purkayastha. (Code available upon request.)