[PL-sem-jr] Planning

[David Herman]

> - I'd love to see a reprise of Dave Herman's dependent types talk.  I
> know what he's talking about, but others are more shaky.  Also, I'm
> hoping a non-HoPL format might spend more time on applications than
> origins.  This might be more enlightening, if there are actually any
> applications to be discussed.

Sure, although I'm presenting in the macros reading group in a couple 
weeks so I'd rather not be the next to present.

> - Before either of those talks, perhaps someone should give a type
> theory primer - make sure we're all on the same page and up to speed.
> Typing inference rules and terms like "simply typed lambda calculus",
> "parametric polymorphism", and "Hindley-Milner inference" should be
> familiar before we delve into our more esoteric topics.

That would be fabulous. And I know there's been a lot of groaning from 
some people in Will's class about writing yet another type checker, but 
it might be instructive to go through the actual code of a simple type 
checker and possibly more importantly a type inferencer. These things 
come to life when you see the code, and they can be a bit too abstract 
when written as inference rules. Actually, come to think of it, showing 
how to interpret inference rules as code might be instructive as well.

Dave