Re: Coq proof assistant

[pezman <mikehogan62@gmail.com>]

@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
>
>