The Coq mailing list

[Greg Morrisett <greg AT eecs.harvard.edu>]

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>