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.