Jason (jcreed) wrote,

Octopus Pie is: A cute webcomic. Whose entire archive is not so long to read through. It runs monday-wednesday-friday.

Things going on today: meetings with Frank and chrisamaphone. Frank found a couple spots in my proof where I was failing to notice certain technicalities, but I think they are easily patched. One curious thing is that, when you have explicit substitutions with variable-for-variable substitutions (i.e. eliminations corresponding to β0-reduction [Dale Miller 1991]) there is another place where you are really testing equality on types that is not merely the synthesis-checking boundary. The other is that in the proof that ξ* really works correctly, you need to notice that the type in the context is in fact underscore-free to pull it across that selfsame boundary.

A historical point that I find interesting is that both the idea of separating inversion from pruning and the idea of inversion-failures showing up as free variables already occur in earlier work — in Tobias Nipkow's 1993 LICS paper, and Dowek-Hardin-Kirchner-Pfenning's JICSLP'96 paper, respectively. All that I've done that's new is proof things about their typing.

Also λs. I should write another real post about that.
Tags: comics, work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded