12 thoughts on “found LJ icon of the day

      1. …and next you’ll be telling me that Γ is a set of typing assumptions, M is a term and τ is a type, but I don’t know what that & is doing in there.

      2. Yeah, that is one of the problems when you’re looking at that shit in a paper and trying to figure out how to translate it into Twelf.

      3. Anyway, I’m curious what type system that’s from; that’s a tough thing to Google (though I’m amused that I wrote one of the top hits for “ftv(τ)”).

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.