The Coq mailing list

[Catherine Dubois <dubois AT ensiie.fr>]

Benjamin Pierce a écrit :
> All,
>
> In the coming semester, as usual, I'll be teaching my course on 
> operational semantics, lambda-calculus, and type systems.  But this 
> time, I'm considering using Coq to present part or all of the material 
> -- both in lectures and in homework assignments.
>
> One of the challenges in this course is that it is pretty large and is 
> mostly taken by masters students, which means that the set of 
> mathematical backgrounds is very diverse; in fact, most of the 
> students have only moderate background in college-level math and none 
> whatsoever in formal logic.  So an important goal of the course is to 
> simply get them comfortable with rigorous (mainly inductive) 
> definitions and proofs.  Doing this with paper proofs in the context 
> of a large class is pretty difficult -- it is nearly impossible to 
> give a large number of people meaningful feedback on written proofs, 
> so they end up not really being able to tell when they are doing it 
> right.  Using Coq is attractive, in part, because it can give them 
> individualized feedback.
>
> Of course, the disadvantage of Coq is that I will need to teach them 
> Coq, and this may be tricky if they have no previous exposure to 
> logic.  I am willing to cut out a little of the current material in 
> the course to make room for this; e.g., if I knew that introducing Coq 
> was going to slow the course down by three weeks, I would probably 
> still do it.  Three months would be a different question.
>
> My questions for the group:
>    - Is this insane?
>    - Have other insane people tried it previously --
>      either in undergraduate / masters level CS courses, or simply for 
> teaching basic logic?
>    - With what results?
>    - Any lecture materials / advice to share?
>
> Many thanks!
>
>     - Benjamin
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
Hi Benjamin

I have been teaching  operational semantics with the help of Coq since 
2003, at ENSIIE  (www.ensiie.fr) (with 15 to 20 students).
I begin with a small introduction to Coq  (about 12 hours and a small 
project). The use of Coq is very precious when induction rule becomes 
necessary.  Students have difficulties to understand that a structural 
induction on commands e.g in a small programming language is not enough.
In parallel we develop interpreters in Ocaml (or typecheckers). My 
students have studied OCaml and functional programming before.

Mathieu Jaume at Paris 6 develops the same approach, cf the paper
David Delahaye <http://cedric.cnam.fr/%7Edelahaye/>, Mathieu Jaume, 
Virgile Prevosto <http://www.mpi-sb.mpg.de/%7Eprevosto/>. /Coq : un 
outil pour l'enseignement 
<http://www-spi.lip6.fr/%7Ejaume/abstracttsi.html>/, Technique et 
Science Informatique,
TSI 24(9):1139-1160, 2005 (in french))


Best regards
Catherine Dubois