coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Greg Morrisett <greg AT eecs.harvard.edu>
- To: Daniel Schepler <dschepler AT gmail.com>
- Cc: coq-club AT inria.fr, Thomas Braibant <thomas.braibant AT gmail.com>
- Subject: Re: [Coq-Club] VSTTE competition (and others sets of problems in general)
- Date: Tue, 5 Jun 2012 12:17:04 -0400
I've always thought that it would be a more interesting contest
if the problems that were posed weren't so focused on imperative
issues in programming (e.g., sort an array using updates). A
more functional-oriented contest would play to the strengths
of not only Coq, but I suspect Isabelle, ACL2, PVS, etc. and
let us do something deeper.
Furthermore, as someone who has written and reasoned about a lot
of imperative code in Coq, I would say that in real developments,
I try hard to minimize the imperative bits. Heck, I find that
to be true when I'm just writing normal code.
Perhaps those who've participated in this contest care to comment?
-Greg
On Jun 4, 2012, at 11:50 PM, Daniel Schepler wrote:
> On Monday, June 04, 2012 06:21:48 PM Thomas Braibant wrote:
>> Hi coq-club,
>>
>> Lately, I had the opportunity to attend a very interesting talk about
>> Dafny [1], which highlighted the recent VSTTE competition (talk about
>> the results at [2]). From the results, it seem that 7 teams made a
>> submission that was using Coq. Unfortunately, I cannot find any using
>> a search engine. So, I am turning to the coq-club list, hoping that
>> some of these people would agree to make their submissions public, and
>> discuss them.
>
> Here's what I did on the competition. I submitted this solution to problem
> 4,
> but did a solution to problem 2 after the deadline. (Although problem 2
> didn't ask for it, I tried proving the uniqueness of one-step reduction of
> S/K
> terms for a little while before giving up.)
>
> (I also posted these solutions on the Google Groups site for the
> competition.
> I don't remember if anybody else posted Coq solutions there.)
> --
> Daniel Schepler
>
> <dschepler.tar.gz>
- [Coq-Club] VSTTE competition (and others sets of problems in general), Thomas Braibant, 06/05/2012
- Re: [Coq-Club] VSTTE competition (and others sets of problems in general), Daniel Schepler, 06/05/2012
- Re: [Coq-Club] VSTTE competition (and others sets of problems in general), Greg Morrisett, 06/05/2012
- Re: [Coq-Club] VSTTE competition (and others sets of problems in general), Jean-Christophe Filliatre, 06/06/2012
- Re: [Coq-Club] VSTTE competition (and others sets of problems in general), Greg Morrisett, 06/06/2012
- Re: [Coq-Club] VSTTE competition (and others sets of problems in general), Jean-Christophe Filliatre, 06/06/2012
- Re: [Coq-Club] VSTTE competition (and others sets of problems in general), Greg Morrisett, 06/05/2012
- Re: [Coq-Club] VSTTE competition (and others sets of problems in general), Jean-Christophe Filliatre, 06/06/2012
- Re: [Coq-Club] VSTTE competition (and others sets of problems in general), Claude Marche, 06/06/2012
- Re: [Coq-Club] VSTTE competition (and others sets of problems in general), Daniel Schepler, 06/05/2012
Archive powered by MHonArc 2.6.18.