Re: Coq proof assistant

[Paul Krause <paul.b.krause@gmail.com>]

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