coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "John Wiegley" <johnw AT newartisans.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] How to show off Coq
- Date: Fri, 30 Jan 2015 15:07:32 -0500
- Organization: New Artisans LLC
>>>>> Eric Mullen
>>>>> <emullen AT cs.washington.edu>
>>>>> writes:
> Specifically, if you were talking to a bunch of undergraduates in Computer
> Science, and you had 10 minutes to convince them that Coq was an awesome
> research tool, what would be your go to example?
Take two types from another programming language that *should* be isomporphic,
and use Coq to prove the isomorphism. Even when I'm not "programming in Coq",
I use Coq as a testbench for proving that my Haskell types fulfill their type
class laws quite often.
This shows not only that Coq is a tool for reasoning that you can trust, but
that you needn't sell the farm to make practical use of Coq right away.
John
- [Coq-Club] How to show off Coq, Eric Mullen, 01/30/2015
- Re: [Coq-Club] How to show off Coq, Adam Chlipala, 01/30/2015
- Re: [Coq-Club] How to show off Coq, Daniel Schepler, 01/31/2015
- Re: [Coq-Club] How to show off Coq, John Wiegley, 01/30/2015
- Re: [Coq-Club] How to show off Coq, Christopher Dutchyn, 01/30/2015
- Re: [Coq-Club] How to show off Coq, Matej Grabovský, 01/30/2015
- Re: [Coq-Club] How to show off Coq, Xavier Leroy, 01/31/2015
- Re: [Coq-Club] How to show off Coq, Louis Garde, 01/31/2015
- Re: [Coq-Club] How to show off Coq, Xavier Leroy, 01/31/2015
- Re: [Coq-Club] How to show off Coq, Gérard Huet, 01/31/2015
- Re: [Coq-Club] How to show off Coq, Greg Morrisett, 01/31/2015
- Re: [Coq-Club] How to show off Coq, Gérard Huet, 01/31/2015
- Re: [Coq-Club] How to show off Coq, Xavier Leroy, 01/31/2015
- Re: [Coq-Club] How to show off Coq, Louis Garde, 01/31/2015
- Re: [Coq-Club] How to show off Coq, Adam Chlipala, 01/30/2015
Archive powered by MHonArc 2.6.18.