My friend Vlad Patryshev organizes the Bay Area Categories And Types meetup. This is a splendid idea, I think. It means people who like the idea of Category Theory and Type Theory can meet and discuss issues, without the pressure of publication and/or competition for spots. I'd love to go more often. I have so far given two talks at BACAT, as we call it.
The first was about partial compilers and dialectica spaces, work of Mihai Budiu,
Joel Galenson and Gordon Plotkin, available from Gordon's webpage. My slides are here Partial Compilers and Dialectica Spaces. (at the talk I discovered that Mihai is actually the husband of an old friend from PARC days...)
The second talk was on even older work with Gavin Bierman, Nick Benton and Martin Hyland, that we never published properly, only in conferences like TLCA and CSL. This is on deriving a term calculus or a type theory for Intuitionistic Linear Logic, together with its categorical models. I find that the best version is still the technical report (Term Assignment for Intuitionistic Linear Logic) from Cambridge. My recent and over-simplified slides are here Linear Type Theory Revisited.
