[TYPES] Who needs a textbook for teaching PL using Coq?
bcpierce at cis.upenn.edu
Fri Jan 23 13:07:59 EST 2009
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
P.S. Here is a little write-up on my experiences with the course last
Also, in case people are interested, here are the complete Fall 2007
version and the ongoing current instance of the course:
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.
More information about the Types-list