I am currently serving as a Senior Software Engineer at QVT Financial LP.
333 River St PH 30
Hoboken NJ 07030
My research interests include programming languages, logical frameworks, type theory, linear and substructural logics, and logic programming. Some of my papers and (CMU access only) drafts are available on my research page.
These notes are often sketchy. This section has not been updated in a while.
Preliminary investigation of certain properties relating to extensionality in an Elf development of HOL, and a variation on the description axiom.
New Elf proof of Hurkens's simplification of Girard's paradox, which states that HOL with polymorphic terms is inconsistent. (Applications: 1. (type : type) leads to the numeralwise representability of all partial recursive functions. 2. There is no polymorphic equality predicate in any extensional model of System F.)
New draft on a representation of HOL Light's core in LF (inspired by Thomas Hales's Flyspeck talk here at CMU).
See the route of a recent bike ride (more or less).