coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.pdfChristophe 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.
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, (continued)
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Benjamin C. Pierce, 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Benjamin Werner, 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Pierre Courtieu, 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/19/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/19/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Jonas Oberhauser, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Kristopher Micinski, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Wolfram Kahl, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Freek Wiedijk, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Jonas Oberhauser, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Wolfram Kahl, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Kristopher Micinski, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Julien Narboux, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/24/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, bertot, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/26/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/26/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Jason Gross, 09/27/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Andrej Bauer, 09/27/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/28/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, bertot, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/24/2012
Archive powered by MHonArc 2.6.18.