Teaching PL using proof assistants

Types and Programming Languages Course with Coq

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

=====
July 28th, The Types Forum, Posted by 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,

=====
Jan 24th, The Types Forum, Posted by 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.