linguistics papers
A number of papers are currently under review. I will add them when they're published or rejected.
logic/type theory papers
 A Tutorial on Categorical Type Theory and Semantics
 A Tutorial on the CurryHoward Correspondence

Abstract: Typical introductions to the CurryHoward Correspondence employ explanations that take the form "a proof of A ∧ B is just a proof of A together with a proof of B, so A ∧ B is just a pair type". This tutorial instead provides a fromscratch explanation, starting with the Natural Deduction proof system for Intuitionistic Propositional Logic with connectives ⊤ ⊥ ∧ ∨ ⇒ . From that, we can easily provide a metaproof system that lets us prove things about Natural Deduction proofs, which will give us precisely the typing rules of the simply typed λ calculus. We’ll also look at how the Natural Deduction rules for proof simplification/normalization give rise directly to the computation rules of the λ calculus.