[TYPES] Teaching PL using proof assistants

[Benjamin Pierce]

Couple of quick questions...

1) I'm putting together a talk for ICFP about using proof assistants  
to teach programming language foundations.  As part of this, I'd like  
to put together a comprehensive list of past experiments in this area  
-- both to educate myself on what's out there and as a resource for  
others.  If you've got a course web site or any other materials that I  
can include, please send me a link.

I'd also love to hear any thoughts or stories you may have.

2) A few months ago I asked here whether other people would be  
interested in teaching their own courses from the Coq-based course  
notes I've been developing over the past couple of years.  I got a lot  
of positive responses, so I've been working to put them in a more  
polished form.  I know of one person already who plans to use them in  
the coming year, and it would be great to have a couple more.  Please  
let me know if you're interested.

Thanks,

    - Benjamin