Stream: Miscellaneous

Topic: Proof Ground 2021


view this post on Zulip maximilian p.l. haslbeck (Mar 29 2021 at 09:00):

Dear Coq enthusiasts,

we are organizing another edition of the proving competition workshop "Proof Ground", which will take place virtually just before ITP 2021.
Please take note of our Call for Problems, and spread the word!


Call for Problems



Proof Ground 2021
Interactive Proving Contest
June 28, 2021
https://www21.in.tum.de/~wimmers/proofground/


at ITP 2021
Interactive Theorem Proving
June 29 - July 2, 2021, (originally in) Rome, Italy, now fully virtual
https://easyconferences.eu/itp2021/


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 is currently used for teaching and hosting proving contests in Coq, Isabelle, and Lean.

Proof Ground 2021 is affiliated with the conference on Interactive Theorem Proving 2021.

As the main conference will happen as virtual conferences due to the ongoing Covid-19 pandemic, Proof Ground 2021 will also take a purely virtual format.

The first edition of the workshop has been held at ITP 2019. The second edition was affiliated with IJCAR 2020.

Important Dates

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:

Submissions from (potential) competition participants are allowed.

Examples can be found at the current "Proving for Fun" contest system, e.g. here.

Submissions can be made via email to wimmers [at] in [dot] tum [dot] de by the date indicated above.

Organizers

Maximilian P. L. Haslbeck
Simon Wimmer
Tobias Nipkow

view this post on Zulip Théo Zimmermann (Mar 29 2021 at 09:36):

@maximilian p.l. haslbeck You should probably send this announcement to coq-club@inria.fr and the Discourse forum (you can do so via e-mail if you prefer at coq+announcements@discoursemail.com) instead of here. All Discourse announcements are forwarded to the Announcements stream here on Zulip (which is otherwise read-only).


Last updated: Aug 19 2022 at 19:03 UTC