The Coq mailing list

[Andr� Hirschowitz <ah AT unice.fr>]

Hello Coq-world!

What about sharing this crazy idea?

I also teach lambda-calculus, together with a few words on PCF. I have 
similar students and I have been thinking about using Coq for years. 
During spring 06, a student made, as her "memoir", a Coq-formalization 
of the proof I gave of Church-Rosser (via parallel reduction). Through 
this,  I wish to mean that the formalization is feasible.

Also we have  at hand  Coqweb (see 
http://www-sop.inria.fr/lemme/Loic.Pottier/pate5.ps), which is designed 
for such (crazy) things: with this, your students do not need specific 
courses on Coq.

Finally there are probably a few people around that could be interested 
in contributing.

So?

ah