Papers & Talks

• Refinement types and computational duality. Submitted, July 2008.
• Duality and polarity in type theory. May 23, 2008. Talk at MFPS 08.
• Polarity and duality in type theory. February 20, 2008. Talk at DTP 08. [agda]
• Focusing on binding and computation. With Dan Licata and Bob Harper. To be presented at LICS 08. [tech report]
• Focusing and higher-order abstract syntax. Presented at POPL 08. [ps] [slides] [errata]
  Coq code:
  • [focusing.tar]: encoding of focused lambda-calculus in Curry-style (untyped syntax, type system and operational semantics, and type safety proof)
  • [focus-church.v]: encoding of focused lambda-calculus in Church-style (typed syntax only)
  • [focusing2.v]: a more general encoding, treating both positive and negative types uniformly. (Revised 27 Feb, 2008.)
  Agda2 code: [polint.agda] (with help from Dan Licata)
• On the unity of duality. Annals of Pure and Applied Logic 153:1 (2008), special issue on "Classical logic and computation". [via Science Direct]
• The logical basis of evaluation order (Thesis proposal). May, 2007. [ps] [slides]

Other Talks

• From AHOS to HOAS. March 4, 2008 at the INRIA Rocquencourt Gallium-Moscova Seminar. [abstract]
• Focusing with higher-order rules. 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. November 3, 2005 at the Rutgers Experimental Mathematics Seminar. [ps]

Notes

• An attempt at a constructive proof of the soundness of labelled deduction for intuitionistic logic. [pdf] [ps] 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".

Et cetera

• Nathack: a natural language interface for nethack. Cassia Martin, David Molnar, Dev Purkayastha, Noam Zeilberger. (Code available upon request.)