The Coq mailing list

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

My bad!  I didn't see that applicative solutions were allowed. In the past, I 
don't think this was the case (or at least not as clear) which is one reason 
I've not participated.  Thanks for correcting me.

-Greg

On Jun 6, 2012, at 4:04 AM, Jean-Christophe Filliatre 
<Jean-Christophe.Filliatre AT lri.fr>
 wrote:

> 
>> 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.
> 
> As two of the organizers, we'd like to comment on this.
> 
> Our problems were not so focused on imperative programming. As stated in 
> the competition description, participants were free to prove purely 
> applicative implementations of the proposed algorithms. And indeed, among 
> the medalists, one gold medal was awarded to a ACL2 solution and one silver 
> medal to a PVS solution. Both were obviously purely applicative. We also 
> received several Coq and Isabelle solutions.
> 
> We deliberately chose an imperative style to describe the problems only to 
> make the competition more accessible to a larger set of participants.
> 
> -- 
> Jean-Christophe and Andrei