Affiliated with
Interactive Theorem Proving 2021
Location: online
The Coq Workshop 2021 is the 12th iteration of the Coq Workshop series. The workshop brings together users, contributors, and developers 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 organized around informal presentations and discussions, supplemented with invited talks.
Due to the ongoing COVID-19 pandemic and the transition of ITP, the conference to which the workshop is affiliated, to an online event, the Coq Workshop 2021 will also be held as an online event.
28.06.2021 The workshop will be held online using Zoom. Registered participants should have received links to access the virtual conference room. We plan to publish recordings of the presentations after the workshop. We have also created a stream on Zulip that can be used to ask questions and continue discussions even after the workshop has finished. We encourage all participants, in particular those who give presentations, to register for the Coq Zulip chat and subscribe to the Coq Workshop 2021 channel.
Talks will be 20 minutes long + 5 minutes for questions
Invited talk: Vincent Laporte: Jasmin: Certified Workbench for High-Assurance and High-Speed Cryptography
| Time (Rome, GMT+2) | Friday, July 2nd, 2021 |
|---|---|
| 10:00 - 10:25 |
Formalization of the Lebesgue Measure in MathComp-Analysis
[abstract] [zulip topic] [slides] [video recording] |
| 10:25 - 10:50 |
Porting the Mathematical Components library to Hierarchy Builder
[abstract] [zulip topic] [slides] [video recording] |
| 10:50 - 11:15 |
A Nix toolbox for reproducible Coq environments, Continuous Integration and artifact reuse
[abstract] [zulip topic] [slides] [video recording] |
| 11:15 - 11:35 | Break |
| 11:35 - 12:00 |
A Toolbox for Mechanised First-Order Logic
[abstract] [zulip topic] [slides] [video recording] |
| 12:00 - 12:25 |
À la Nelson-Oppen Combination for congruence, lia and lra
[abstract] [zulip topic] [slides] [video recording] |
| 12:25 - 12:50 |
General automation in Coq through modular transformations
[abstract] [zulip topic] [slides] [video recording] |
| 12:50 - 14:20 | Lunch break |
| 14:20 - 15:00 |
Invited talk: Jasmin: Certified Workbench for High-Assurance and High-Speed Cryptography
[zulip topic] [slides] [video recording] |
| 15:00 - 15:25 |
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
[abstract] [zulip topic] [slides] [video recording] |
| 15:25 - 15:50 |
Extending MetaCoq Erasure: Extraction to Rust and Elm
[abstract] [zulip topic] [slides] [video recording] |
| 15:50 - 16:10 | Break |
| 16:10 - 16:35 |
Certifying assembly optimizations in Coq by symbolic execution with hash-consing
[abstract] [zulip topic] [slides] [video recording] |
| 16:35 - 17:00 |
Coq/Ssreflect for large case-based graph theory proofs
[abstract] [zulip topic] [slides] [video recording] |
| 17:00 - 17:30 | Coq Development Team [slides] [video recording] |
Authors should submit extended abstracts through EasyChair.
Relevant subject matter includes but is not limited to:
Talk proposals should be no more than 2 pages in length including bibliographic references using the EasyChair style with the fullpage package. All submissions must be in PDF format.
Christian Dozkal and Jean-Marie Madiot (coq2021@easychair.org)