coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proving for Fun: Summer Edition

From: Armaël Guéneau <armael.gueneau AT ens-lyon.fr>
To: coq-club AT inria.fr
Cc: "Maximilian P. L. Haslbeck" <haslbema AT in.tum.de>, Simon Wimmer <wimmers AT in.tum.de>
Subject: [Coq-Club] Proving for Fun: Summer Edition
Date: Fri, 5 Jul 2019 19:36:21 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=armael.gueneau AT ens-lyon.fr; spf=Pass smtp.mailfrom=armael.gueneau AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Ironport-phdr: 9a23:IUYzaRDVY4aV2hKqzBM/UyQJP3N1i/DPJgcQr6AfoPdwSPT9r8bcNUDSrc9gkEXOFd2Cra4d0ayN7+u5ADdIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfK1+IA+4oAjeucUanJZuJ6gswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKLCAy/n3JhcNsjaJbuBOhqAJ5w47Ie4GeKf5ycrrAcd8GWWZNW8BcXDFDDIyhdYsCF/QPM+ZFoYf+qVUBoxSxChWjCu701j9FhWX70bEm3+kvEwzL2hErEdIUsHTTqdX4LLsfUfqwzKbS0TLDa+tZ1zbg6I/SdBAuv+uDXa9tesfW00YvDQbFgU+OpozhJT+V2fkNvHad7+V+T+2vlnUqpB93oji038ssjonIhoUTylze+yV52p84KNulQ0B1Zt6kFYFftyCcN4ZuXsMiXmRotDwnxbIYoZK7fTMKx448yBHBb/yHd5aH7gj4VOeROjd4mGxqeLekhxu07EOuyfX8W9Gp3FtFsiZJiNvBu3IX2xDO68WKSOFx8lm/1TqRzwze6eJJLVopmaffNpIt2KM8m5sNvUjZAyP7m0f7gamLfUs+4Oeo8f7oYrD+q5+cKYB0jgb+P7wqmsOlGus3KRYBU3KF9uS6z73v5En5QbVNjv0wiKXZvoraKdwapq6/HQBVzp4u5wuwAju6ytgVn3sKIEhYdB+GjYXlIU/CLO7mAfunhlSjijZrx/TIPr37BZXNK2DOn637fbZ48UFT1g4zwcpQ55JJFL4BJuz8VVXstNHDEBA5NRe0z//jCNR90YMeX3iDAqGDMK/Kq1+H+vovI/WQZI8SoDvyN/8l5+f3gXAlnV8dYLKm0IAMaHG4G/RmO1+WbWDtgtcHC2cKvxAxQPbkiF2YAnZvYCO5WLt57TUmAqqnC53CT8ajmu+vxiC+S7RMY2nFDmejDPbueoyZE6MFciebL8snnSEJU7WoVqcs0wrrsB79zfxpNLyHqWUjqZv/2Y0ttKXonhYo+GkxVpzFijzffyRPhmoNAgQO8uV/rEh6kwbR1aFyifEeGNpIovdYVQF8O4SOl7UmWeC3YRrIe5KycHjjWs+vWGpjQ9QqhtsfZEA7Fc/w1kmSjRrvOKcckvmwPLJx96vd23brIMMkkCTL0rJki0ghRI1BLz//iw==

Dear Coq enthusiasts,

We are happy to announce a new proving contest at Proving for Fun, an
online platform where you can tackle proving challenges in your favorite
proof assistant:

https://competition.isabelle.systems/competitions/contest/11/

This month's contest features freshly implemented support for Coq. This
means you can now submit your solutions in both Isabelle and Coq. The
contest is open starting now until 9 August 2019.

This also serves as a warmup for the "Proof Ground" workshop [1], which
will take place in September alongside the ITP conference in Portland.
The goal of the workshop is to bring together researchers from the ITP
community, to discuss and compete in a "proving contest", and it will
use the Proving for Fun platform. If you happen to have ideas for
interesting tasks, please consider submitting them following our "Call
for Problems".

We believe our problems should be a stimulating fun summer activity! We
encourage you to participate and give us feedback on the prototype system.

Happy proving,

Armaël Guéneau
Max Haslbeck
Simon Wimmer

[1] https://www21.in.tum.de/~wimmers/proofground/

[Coq-Club] Proving for Fun: Summer Edition, Armaël Guéneau, 07/05/2019