Re: Coq proof assistant

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

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