Hi! Bonjour! Привет!
I’m a PhD candidate in computer science at Carnegie Mellon University and a Debian Developer. My professional ambition is to do beautiful mathematics that are relevant to computer science. I’m generally interested in the semantics of programming languages, the CurryHowardLambek isomorphism, parametric polymorphism, and the foundations of mathematics.
While an undergraduate, I had the opportunity to do research at several wonderful places: McGill University, Microsoft Research Cambridge, Queen’s University’s School of Computing, MIT CSAIL, and ENS Lyon. I also spent a semester studying at the Independent University of Moscow in their “Math in Moscow” programme. A copy of my CV is available here.
See my blog for my musings on computer science, mathematics, and languages—spoken or otherwise.
Recent Blog Posts

Presheaf categories are Cartesian closed
As I’ve been working through “Sheaves in Geometry and Logic”, I’ve been skimming proofs and attempting to rederive them. I normally end up with a better understanding of the material, but sometimes I get stuck. Here’s one case where I’ve gotten stuck: can anybody tell me why the counit for... 
Configuring CMU SCS printers on Linux
Unless your Linux host was “facilitized” (i.e., unless you’re still running the stock Linux install provided by the CMU help desk), you’re probably scratching your head as to how to add SCS printers to your Linux host. Here’s how. (NOTE: You should only add SCS printers if you have an... 
Specifying a custom MTA path in caff
I recently had to sign someone’s GPG key. I’ve long used the caff tool from the signingparty package to help me with this. Unfortunately, I’m using a new laptop and hadn’t yet configured caff on it. Moreover, caff uses the system MTA by default, normally found at /usr/sbin/sendmail, and I... 
The Yoneda Lemma
I had never before realised the immense usefulness of the Yoneda lemma. In the past few sections of Mac Lane’s and Moerdijk’s “Sheaves in Geometry and Logic”, it’s been used both as a proof tool and as a heuristic for finding the right definition of a functor (in this case,... 
On terminal objects and colimits
I’m currently working through Mac Lane’s and Moerdijk’s “Sheaves in Geometry and Logic”, and came upon the following two sentences in a proof (p. 43): Note that when is representable the corresponding category of elements has a terminal object—the element of . Therefore the colimit of the composite will just...
subscribe via RSS