The Coq Workshop 2024 is the 15th instalment of the Coq Workshop series. The workshop brings together developers, contributors, and users of the Coq proof assistant. The Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, rather than serving as a venue for traditional research papers, the workshop is organised around informal presentations and discussions.
Important dates
29 May 7 June, 2024 (AoE)
Submission deadline (⚠️ extended)
3 July, 2024
Author notification
Attending
As the workshop is affiliated with ITP, attendees are required to register for the workshop through ITP registration. The workshop (as well as the conference) can be attended either online or in person. Please consult the ITP registration page for pricing information.
One of the sessions will be affiliated with EuroProofNet. As such participants of the Coq Workshop are also entitled to funding from EuroProofNet.
See the EuroProofNet workshop website for more details.
Program
The following contributed talks were accepted for a presentation at the workshop.
Lessons from Formalizing (Higher) Category Theory
Benedikt Ahrens and Niels van der Weide
On the Potential of Coq as the Platform of Choice for Hardware Design
Sebastian Ertel, Max Kurze and Michael Raitza
CoqPilot, a plugin for LLM-based generation of proofs
Andrei Kozyrev, Gleb Solovev, Nikita Khramov and Anton Podkopaev
Coq Platform docs: A Compilation of Short Interactive Tutorials and How-To Guides for Coq
Thomas Lamiaux, Pierre Rousselin and Théo Zimmermann
Blueprints for formalisation in Coq
Peter Lefanu Lumsdaine
Turning the Coq Proof Assistant into a Pocket Calculator
Guillaume Melquiond
Towards Formalising the Guard Condition of Coq
Yee Jian Tan and Yannick Forster
A Development Process for Coq Projects Permitting Invalid Proofs
Hendrik Tews
Submission instructions
Submissions should take the form of a two-page PDF (excluding bibliography) and must be performed on Easychair.
You have the freedom to produce the PDF by whatever means but keep in mind that it should remain legible for the people of the PC and for attendees of the conference so please avoid two pages of text with absolutely no margin.
We use a single-blind review process, meaning that reviewers have access to the identity and affiliations of the authors. As such, the submitted PDF should include name and affiliations in addition to the title and abstract.
Remote presentation is possible!
Submit to Coq Workshop 2024Program committee
- Benedikt Ahrens (TU Delft)
- Mireia González (Formal Vindications)
- Mirai Ikebuchi (Kyoto University)
- Assia Mahboubi (Inria Rennes)
- Clément Pit-Claudel (EPFL) [chair]
- Swarn Priya (Virginia Tech)
- Michael Sammler (ETH Zürich)
- Enrico Tassi (Inria Sophia)
- Théo Winterhalter (Inria Saclay) [chair]
- Irene Yoon (Inria Paris)
- Yannick Zakowski (Inria Lyon)