The Coq mailing list

[Armaël Guéneau <armael.gueneau AT ens-lyon.org>]

Dear Coq enthusiasts,



------------------------------------------------------

Call for Problems

------------------------------------------------------



------------------------------------------------------

Proof Ground 2020

Interactive Proving Contest

June 29, 2020

https://www21.in.tum.de/~wimmers/proofground/

------------------------------------------------------

at IJCAR 2020

International Joint Conference on Automated Reasoning

June 29 - July 5, 2020, (originally in) Paris, France
, now virtual
https://ijcar2020.org/

------------------------------------------------------



This workshop brings together researchers of the ITP community to
compete in a "proving contest".



While programming contests (e.g. ACM ICPC, International Olympiad in

Informatics) challenge large numbers of participants to solve

algorithmic problems within a short time, we envision proving contests

to entice proof engineers to formally prove small but interesting

problems from mathematics or computer science.



A contest system (https://competition.isabelle.systems/) is currently
used for teaching and hosting proving contests in Coq, Isabelle, and Lean.



Proof Ground 2020 is part of the Paris Nord Summer of LoVe 2020
(https://lipn.univ-paris13.fr/summer-of-love-2020/), a joint event on
LOgic and VErification at Université Paris 13,

made of Petri Nets 2020, IJCAR 2020, FSCD 2020, and over 20 satellite
events.



As the main conferences of Paris Nord Summer of LoVe will happen as
virtual conferences due to the Covid-19 outbreak, Proof Ground will also
take a purely virtual format.



The first edition (https://www21.in.tum.de/~wimmers/proofground2019/) of
the workshop has been held at ITP 2019 (https://itp19.cecs.pdx.edu/).



Important Dates



   Submission deadline: June 1, 2020



   Workshop and Competition:  June 27, 2020



Call for Problems



   In order to conduct a stimulating contest we solicit interesting tasks.



   A contest typically lasts for two hours and consists of around five

   problems with varying difficulty.



   A problem:



   -   should contain an informal statement of the problem together with
       a template for the formal proof;



   -   should come with a reference solution (in any ITP);



   -   should be solvable (including formal proof) within 30 minutes;



   -   should be easy to state in any proof assistant, without requiring

       too much background library;



   -   could be from any part of mathematics, software verification, or

       your daily work with ITPs, and could also be a logic
       puzzle/riddle;



   -   could contain several subproblems which lead to partial points.



   Submissions from (potential) competition participants are allowed.



   Examples can be found at the current "Proving for Fun" contest system,

   e.g. here (https://competition.isabelle.systems/competitions/contest/6/).



   Submissions can be made via email to

   wimmers [at] in [dot] tum [dot] de by the date indicated above.



Organizers



   Maximilian P. L. Haslbeck

   Tobias Nipkow

   Simon Wimmer