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

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

*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]

*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]

*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.)