Re: Coq proof assistant

[Dan Mead <d.w.mead@gmail.com>]

learning coq has been on my to do list for a while

is there a good introduction to it you could recommend Michael?

I studied theorem proving for a bit as an undergrad, but I've never
been exposed
to full blown logic systems.

-dan

On Tue, Nov 24, 2009 at 9:59 PM, Michael Greenberg
<michael.m.greenberg@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
>