The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Wed, 13 Jun 2007 13:14:35 +0100,
Benjamin Pierce 
<bcpierce AT cis.upenn.edu>
 a écrit :

> Many thanks to everyone for the encouragement and pointers so far.   
> On the basis of what I've heard, I remain very tempted to try the  
> experiment this Fall, so please keep the suggestions coming!  :-)
> 
>      - Benjamin


Let me take this occasion to advertise the RDP affiliated
workshop PATE (proof assistants and types in education
http://www.rdp07.org/pate.html), which is exactly on this topic.

Maybe you can still register to RDP (June 25, 2007 to Friday, June
29 http://www.rdp07.org)!

Best regards,

Pierre Courtieu

---------------------------8X-----------------------------

Program of PATE:

9:00-10:30
        Bill Farmer  (invited speaker)
        "The Use of Formal Reasoning Technology in Mathematics
Education: Opportunities and Challenges" 

        Claudio Sacerdoti Coen -  Enrico Zoli
        "A Note on Formalising Undefined Terms in Real Analysis"

10:30-11:00 coffee break

11:00-12:30
        Agnieszka Kozubek - Pawel Urzyczyn
        "In the search of a naive type theory"

        Adam Naumowicz
        "How to Teach to Write a Proof"

        Serge Autexier - Marc Wagner
        "Status Report on the Tight Integration of a Scientific 
        Text-Editor and a Proof Assistance System"

12:30-14:00 lunch

14:00-15:30
        Jérémy Blanc - André Hirschowitz - Loïc Pottier
        "Proofs for freshmen with Coqweb"

        Cezary Kaliszyk - Freek Wiedijk - Maxim Hendriks - Femke van
Raamsdonk "Teaching logic using a state-of-the-art proof assistant"

        Jakub Sakowicz - Jacek Chrzaszcz
        "Papuq: a Coq assistant"
        
15:30-16:00 coffee break

16:00-17:00
        René David - Christophe Raffalli
        "Some considerations about proof assistants for education"