|
[Date Prev] [Date Next] [Thread Prev] [Thread Next] [Date Index] [Thread Index]
- From: Paul Krause <paul.b.krause@gmail.com>
- To: Philly Lambda <philly-lambda@googlegroups.com>
- Subject: Coq proof assistant
- Date: Tue, 24 Nov 2009 14:56:54 -0800 (PST)
- Dkim-signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:x-beenthere:received:received:received :received:received:received-spf:received:mime-version:received:date :x-ip:user-agent:x-http-useragent:message-id:subject:from:to :reply-to:precedence:mailing-list:list-id:list-post:list-help :list-archive:x-thread-url:x-message-url:list-unsubscribe :list-subscribe:content-type; bh=AX7stpCU4Z2vuwJ2vkYRhG+DVAb6T9F+HZHI0OeITUQ=; b=IFz+RkKnLMlSJ1jc6AtqEByUdjqqVHZ/SDA+SGlHkDc0XUEQjHMjzdvP3S+lgmevn6 RV5HnIRYOGV/Qsj5OGBrEWGuEQ4S12x0RO3/Jr4nlyR+aF+dDmXdOpFasbNrIgQbZyiK XcXDX/+4Az5zfmYm6ndMp3ilokli3h8U4TBqg=
- List-archive: <http://groups.google.com/group/philly-lambda?hl=>
- Mailing-list: list philly-lambda@googlegroups.com; contact philly-lambda+owners@googlegroups.com
- Reply-to: philly-lambda@googlegroups.com
- User-agent: G2/1.0
Hey, has anyone had any experience with Coq? It's a tool (written in
ocaml) for doing a number of things (like assist in solving proofs of
course, and also generating code that's provably correct). I've been
playing around with it and I've found it both frustrating and
fascinating.
One thing that made me think that it might be of interest to some in
this group is it's based on a form of typed lambda calculus, and, you
know, Philly-<i>Lambda</i>. Also, one of the languages that it
supports generating certified programs for is Haskell, a language that
I gather has something of a following here (also ocaml).
I just wanted to put out some feelers to see if anyone else had any
experience on it and maybe compare notes, or had any experience with
other/preferred tools in a similar vein (i.e. proof assistants).
Paul
|
|