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 Curry-Howard Correspondence

Abstract: Typical introductions to the Curry-Howard 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 from-scratch explanation, starting with the Natural Deduction proof system for Intuitionistic Propositional Logic with connectives ⊤ ⊥ ∧ ∨ ⇒ . From that, we can easily provide a meta-proof 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.