Drafts, Slides, Unpublished Work
My TeX Macros
My BibTeX File

Focused Linear Semantics of Modal Logic
Focusing as Token-Passing
Queue Logic: An Undisplayable Logic?
Notes on Labelling Linear Logic
A Judgmental Deconstruction of Modal Logic
Focalizing Linear Logic in Itself
Speculations on Weak ω-structures
Names are (mostly) Useless (WMM'08)
Names via Substructural and Dependent Types (draft talk slides)
Translating Focusing into Ordered Logic
Base-Type Polymorphism in LF
Cyclic Dependent Types
TinyLF: A Compact Definition of a Logical Framework
Properties of Hereditary Substitution without Type Indices
Modular Proof of Completeness of Focusing
[PS] [Twelf]
Terminating Untyped Hereditary Substitution
The Identity Theorem in Hereditary Spine Form
A Comonadic Generalization of Top
Labelled LF Notes
Canonical Forms in a Hybrid Logical Framework

Proof Irrelevance with Hereditary Substitution
[LaTeX] [PDF]
Letcc elimination in labelled natural deduction

Slides for seminar talk on EML
Classical Truth as a Modal Operator
Slides for TPHOLs 2003 talk
Revision of (Pfenning LICS'01)
(Work in progress)
Proof Irrelevance in a Logical Framework
(Senior Thesis Extended Abstract, work in progress)
LF with Irrelevance and Notational Definitions
(Senior Thesis research in progress)
Slides on the Join Calculus
(Slides for my 15-819 Seminar on Languages for Mobile Computation talk, Fall 2001)
[LaTeX] [PS (2)]
Notes on MacLane & Moerdijk Chapter IV
(Notes for my 80-820 Topos Theory Seminar talk, Spring 2001)
Notes on Split Coequalizers
Notes on the internal category functor
(Contains conjectures I later found out to be well-known falsehoods)
[TeX] [DVI]
Priorities and Comonads
(Actually, the idea of semimonads (a "priority" as defined here is a sort of semicomonad) does appear in the literature in the more general setting of 2-categories, but I lost the reference. Somewhere in an Australian Mathematical Society journal, if I remember correctly)
[LaTeX] [DVI]