The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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

Attachment: dschepler.tar.gz
Description: application/compressed-tar