Lambda the Ultimate

We will be publishing online the materials (slides, exercises, etc.) for the tutorial afterwards. We're aiming to make the materials useful both for those who do attend the tutorial (e.g., additional exercises we won't have time to get to) and for those who are looking at them "off-line" (e.g., plenty of written comments and explanations).

(Just to be clear, I am one of the many people helping organize this tutorial.)

Take a look at this post, including comments. You should find a few more pointers to tutorials and ideas about how to begin studying.

A Syntactic Approach to Type Soundness would be one.

See also here (and revive the old thread if you want).

...about a useful introductory path can be found here.

...get the Coq'Art book. Do spend the money, if you will spend the time.

According to Michael Greenberg (hi, Michael! It was nice to meet you at the tutorial), U Penn's CIS 500 course covers essentially the same material as the tutorial did—it just does so in a semester rather than one day. :-) The CIS 500 course materials can be found here. What's perhaps a bit confusing at first is that the "lectures" linked to are, in fact, Coq .v files.

I should point out that all of these Coq developments are extremely heavily commented and the introductory materials (CoqIntro.v, STLCTutorial.v) are self-contained: it's possible to work through them without reference to anything else and they assume no prior experience. They also reflect the high writing standards that we've come to expect from the Computer Science department at U Penn.

In summary, the in-person tutorial at POPL '08 was exactly the breakneck-paced, whirlwind slide down the rabbit hole that I had hoped it would be—honestly, I can't recall the last time I had that panicky I'm-falling-behind-and-I'll-never-catch-up feeling and paid good money for it. The last time I was in school, I suppose. :-) The U Penn team were well-prepared, with printouts; CDs containing all of the software, documentation, IDEs, and tutorial files; and tremendous patience with us newcomers. The pace really was breakneck, but it had to be given the scope: zero to progress and preservation for the simply-typed lambda calculus in one day. Somehow, though, they seemed to keep their fingers on the pulse of the group, dropping exercises, giving a few more minutes for people to complete their work, helping out both during the exercise time and during breaks, etc.

For those who are interested but couldn't attend, I can't recommend the tutorial materials proper and U Penn's CIS 500 materials strongly enough. It's also worth keeping in mind that in some ways, this really was the coming-out party for U Penn's metatheory library for Coq, which has already seen third-party use and gotten positive feedback, as I commented on here.