Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] VSTTE competition (and others sets of problems in general)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] VSTTE competition (and others sets of problems in general)


Chronological Thread 
  • 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>




Archive powered by MHonArc 2.6.18.

Top of Page