[TYPES] Who needs a textbook for teaching PL using Coq?

[Benjamin Pierce]

For the past couple of years, I've been working on developing course  
materials for teaching basic theory of programming languages using a  
proof assistant.  Last year I taught a semester-long course to a  
mixture of undergraduates, Masters, and beginning PhD students,  
covering elements of functional programming, constructive logic,  
theorem proving, operational semantics, and types, with 100% of the  
lectures and homeworks fully mechanized in Coq.  I found this approach  
worked amazingly well: the interactivity enabled by Coq was extremely  
motivating for students, and both the stronger *and* the weaker  
students performed better on exams than in previous years where I'd  
delivered similar material with blackboard, paper, and pencil.   
Encouraged by this success, I am working this semester on a second  
revision of the material.

Since I'm producing reasonably complete lecture notes, I've naturally  
begun to wonder whether it would be worth putting in the extra work  
required to turn these notes into a proper book.  But since this work  
is inevitably going to be significant, I'd like to try to get an idea  
how many people out there might actually use such a book.  So...

If this sounds like a course that you would teach if a textbook for it  
existed, could you please drop me a note?  I'd be interested in how  
many (and what level) students you think would take such a course at  
your institution, how often you'd think of offering it, whether you  
already teach a course covering related material, and what book you  
use now for this course.  I'd also be interested in hearing from  
people that would want to use such a book for self study, or from  
anyone who has any thoughts at all about what such a book should be  
like.

Many thanks!

     - Benjamin

P.S.  Here is a little write-up on my experiences with the course last  
year:

     http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf

Also, in case people are interested, here are the complete Fall 2007  
version and the ongoing current instance of the course:

     http://www.seas.upenn.edu/~cis500/cis500-s09/index.html
     http://www.seas.upenn.edu/~cis500/cis500-f07/index.html

The coverage of material this time will be similar to last year,  
except that I'll drop the untyped lambda-calculus in favor of a module  
on simple while-programs, including a little Hoare logic.