The Coq mailing list

[Aaron Stump <stump AT mail.cse.wustl.edu>]

Hi, Benjamin.  I used Coq in my undergraduate Logic and Discrete Math
class Spring 2006 and Spring 2007.  Spring 2006, I emphasized natural
deduction proofs and set theory, with induction coming later.  This
ended up being, it seems, pretty dry and tedious for students.  Spring
2007 I put induction and program verification first, as the more
compelling applications for aspiring Computer Scientists.  I did not
even try to do set theory in Coq.  Also, in 2007, the course staff had
required weekly lab/studio sessions (we actually used class time for
this) on Coq.  The focus on induction and program verification together
with the lab support seems to have worked.  Students appeared to enjoy
using Coq more in the 2007 version, and they did not have too much
trouble picking it up in 3-4 weeks.  

Both semesters, I wrote short draft books, which are freely available
from the course web sites, together with homeworks.  The Spring 2006
version reflects the focus on natural deduction, while the Spring 2007
version is more geared towards induction and program verification.

Both semesters, I completely avoided the more advanced aspects of Coq's
type theory.  I imagine for a programming languages theory course, more
of this would be needed; for example, more elaborate indexed types for
representing typing derivations.  We did not touch such features in the
undergraduate classes.

The course web sites are linked from the "Classes" section of
my group's web page: cl.cse.wustl.edu.

Hope this may be helpful!
Aaron