Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Interest in Coq-based mathematics classes?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Interest in Coq-based mathematics classes?


Chronological Thread 
  • From: Julien Narboux <jnarboux AT narboux.fr>
  • To: Adam Chlipala <adamc AT csail.mit.edu>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Interest in Coq-based mathematics classes?
  • Date: Thu, 20 Sep 2012 10:50:56 +0200

HI Adam,

In France, André Hirschowitz and Loic Pottier and Xiao Gang have performed some experiments about using Coq to teach mathematics.

see:http://math.unice.fr/~ah/div/bghp.pdf

Christophe Raffalli is also using his own tool called Phox to teach maths:
http://www.lama.univ-savoie.fr/~raffalli/?page=cours&lang=fr

Cheers,

Julien

2012/9/17 Adam Chlipala <adamc AT csail.mit.edu>
I'm interested in applying Coq in teaching university students mathematical subjects, including the theory underlying computing.  This message is meant to get a sense of who out there is interested in collaborating to build the necessary tool support.

A bit of my personal context: I teach at MIT, which has a newish initiative MITx, for running online classes, with opportunities to apply the same technology to augment traditional in-person education.  Automatic grading is a central part of the approach, and one of the biggest scaling challenges has been grading assignments where students write mathematical proofs.  I think Coq is the secret weapon for addressing this challenge, but I also think we need some new tool and library support to present Coq in a way that doesn't send first-year university students running and screaming.  I'm doing some initial work in this direction with students, but I think this is an idea that could really benefit from a broad community effort.

So, I have two primary questions to ask:

1. Would any Coq experts be interested in spending some time at MIT as postdocs or research scientists, building the support for applying Coq in early university classes relevant to computer science?  Please let me know if so!

2. Could we as a community create an open platform for contributing Coq libraries relevant to different modules of different courses?  A nice user interface would be crucial, and it wouldn't be any good for each university to roll its own.  I would like to see a web-based interface, with bonus points (from my perspective) if it uses my language Ur/Web <http://www.impredicative.com/ur/>. :)  I also feel that we need course-specific tactic libraries, to allow proofs to be written at the right levels of abstraction, without overwhelming students.





Archive powered by MHonArc 2.6.18.

Top of Page