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: 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.
>



Archive powered by MHonArc 2.6.18.

Top of Page