coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: immanuel litzroth <ilitzroth AT gmail.com>
- 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: Mon, 17 Sep 2012 20:57:45 +0200
Hi Adam,
I for one would be very interested. I'm currently doing a MITx course
in electronics
on the advice of one of my colleagues and I'm very much enjoying it. Moreover
at
my workplace (I do C++ programming) there are several people who have
expressed
frustration in learning and using coq -- we do have some stuff the we
would like to "prove
correct" -- so I guess I'd be bringing between 3 and 6 people along!
Kind Regards,
Immanuel Litzroth
On Mon, Sep 17, 2012 at 7:47 PM, Adam Chlipala
<adamc AT csail.mit.edu>
wrote:
> 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.
>
- [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/17/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, immanuel litzroth, 09/17/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Andrej Bauer, 09/17/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Kristopher Micinski, 09/17/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Edward Z. Yang, 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Pierce Benjamin C., 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Kristopher Micinski, 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Kristopher Micinski, 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Benjamin C. Pierce, 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Kristopher Micinski, 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Pierce Benjamin C., 09/18/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Edward Z. Yang, 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?, Kristopher Micinski, 09/17/2012
Archive powered by MHonArc 2.6.18.