Frantic scribbling

By Dann

Dearest Humans,

We had a perfectly lovely meeting this past Friday, full of tasty sandwiches, frothy beverages and even frothier musings as we stewed over a Greek alphabet soup of a proof. Questions were answered, confusionations were clarified (though a few were left dangling – how do we account for the lack of generics in Thm1.iv?), and we reveled in the joys of structural induction as a group for the first time. There was frantic scribbling in notebooks, hasty flipping back and forth through the paper to verify claims, deep discussion on impossibly tiny but incredibly crucial minutia, and an awful lot of pensive staring into middle distance: in short, we did math.

Thanks again to Pete for leading us from the dark and foreboding woods into the light of understanding. This week Ben has stepped up to the challenge of guiding our minds through Algorithm W and on to the proof of its soundness. We’ll forge as far into section 4 as we are able this week, finish the paper off next week, take a week off and then launch into typed meta-programming like an unstoppable force meeting a slightly-less-than-unmovable object.

As a side benefit of diving deep into the proof of the Semantic Soundness Theorem, the challenge to implement Algorithm W – or a suitable interpreter for the language it is described in – is still open, so dust off your space cadet keyboard and get ready to hit a few six key chord combos.

Love and Lambdas Dann?