Re: Coq proof assistant

[pezman <mikehogan62@gmail.com>]

It looks like Paul and I are going to take a stab at working through
the SL material.  If anyone else wants to participate, please drop
either of us a line.  I think that we're tentatively shooting at a
chapter per week with occasional "lazy weeks" (say 10 or 11 days) to
accommodate holidays and/or give difficult material a little more soak
time.

Michael Greenberg did request that we be careful about keeping
solutions out of view.  Other than that, there seems to be nothing but
love ...

@MG -- I was wondering if there is any material under development that
goes deeper into TAPL stuff or other PL topics that might be of
general interest?  I'd love to get the gut feel for the more advanced
topics in TAPL (System F, F-omega etc.) and topics in intensional type
systems etc. etc.  It might be fun to beta-test some stuff like that
(otoh, we might be unqualified test subjects).




On Nov 30, 8:07 am, Paul Krause <paul.b.kra...@gmail.com> wrote:
> Mike (or anyone else), I would like to second the interest in seeing a
> talk on this topic.
>
> On Nov 29, 7:27 pm, pezman <mikehoga...@gmail.com> wrote:
>
>
>
> > @Mike,
>
> > Would you or anyone else in the PL group be willing to give a talk on
> > the topic?
>
> > @anyone else
> > If anyone wants to work through the book in a semi-formal way, I'm
> > game.  I have taken the course before, but would be happy to refresh.
> > I can attest that the slides and exercises are pretty well suited to
> > self-study.  However, it's probably handy to have a partner for the
> > exercises -- some of them are pretty challenging.
>
> > On a somewhat different note, I really wish the INRIA guys had
> > selected a different name.  I'm sure that they know that this is a
> > terrible name in English.  Revenge would be sweet -- maybe a regular
> > expression-like query language for polymorphic regular tree types
> > called "Kleene Inductive Query Type and Term Engine", or KIQUETTE for
> > short. Imagine a class full of French grad students reduced to
> > snickering like Beavis and Butthead, or the incredibly awkward things
> > that would inevitably be said (in French) while discussing this in
> > department meetings.  Just an idea ...
>
> > On Nov 25, 8:11 am, Paul Krause <paul.b.kra...@gmail.com> wrote:
>
> > > Michael, thanks for the pointers.  Now I'll have something to occupy
> > > myself over the long weekend ;).
>
> > > The Software Foundations book looks good, and should go some way
> > > towards helping me work through my areas of incomprehension.  I do
> > > have the Bertot-Casteran book, which I like a lot, but there are still
> > > things I'm having trouble understanding.  This looks like it might
> > > help.
>
> > > I love the 'assembly language of theorem proving' joke; spot on the
> > > money.
>
> > > I'll also check out Agda and see what I think.
>
> > > I'm sure I'll have some concrete questions at some point, but let me
> > > chew on the links you sent for a bit and see where that gets me.
>
> > > Thanks again,
> > > Paul
>
> > > On Nov 24, 9:59 pm, Michael Greenberg <michael.m.greenb...@gmail.com>
> > > wrote:
>
> > > > Hi Paul,
>
> > > > Coq is a great tool!  Penn (where I am a PhD student) is a big Coq
> > > > school. ;)  We're the home of the POPLmark challenge
> > > > (http://alliance.seas.upenn.edu/~plclub/cgi-bin/poplmark/) which
> > > > exercises Coq (among other provers).  Benjamin Pierce, Chris
> > > > Casinghino and I wrote Software Foundations
> > > > (http://www.cis.upenn.edu/~bcpierce/sf/), the course book for CIS 500,
> > > > the graduate level introduction to programming languages.  It uses Coq
> > > > to teach functional programming, simple imperative programs, the
> > > > simply-typed lambda calculus, and a few extensions to the lambda
> > > > calculus.  Naturally, I think it's a pretty good introduction to Coq.
> > > > :)  Some other Penn people---in particular, Aaron Bohannon and Brian
> > > > Aydemir---put on a (great!) tutorial at POPL08 in San Francisco
> > > > (http://www.cis.upenn.edu/~plclub/popl08-tutorial/).  It's targeted at
> > > > a rather technical audience, but it offers more realistic developments
> > > > than our book.  I hope some of those resources are useful for you.
>
> > > > I agree that Coq can be frustrating.  Some of us joke that Coq is the
> > > > assembly language of theorem proving---for example, it doesn't
> > > > directly support dependent pattern matching, so tactics have to
> > > > manually construct equalities.  At a higher level, I'm sometimes
> > > > frustrated by the rigidity of the tactic language.  (Though I haven't
> > > > tried using Ltac, which I hear is quite helpful.)  If you're looking
> > > > for alternatives, Agda is a general-purpose Haskell-inspired theorem
> > > > prover based on dependent pattern matching that some other people in
> > > > the department like.
>
> > > > Cheers,
> > > > Michael