The Coq Workshop 2021

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.

COVID-19 notice

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.


To participate, please register for the workshops associated with ITP via Easy Conferences.


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 Reynald Affeldt and Cyril Cohen
[abstract] [zulip topic] [slides] [video recording]
10:25 - 10:50 Porting the Mathematical Components library to Hierarchy Builder Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Théry and Anton Trunov
[abstract] [zulip topic] [slides] [video recording]
10:50 - 11:15 A Nix toolbox for reproducible Coq environments, Continuous Integration and artifact reuse Cyril Cohen and Théo Zimmermann
[abstract] [zulip topic] [slides] [video recording]
11:15 - 11:35Break
11:35 - 12:00 A Toolbox for Mechanised First-Order Logic Johannes Hostert, Mark Koch and Dominik Kirst
[abstract] [zulip topic] [slides] [video recording]
12:00 - 12:25 À la Nelson-Oppen Combination for congruence, lia and lra Frédéric Besson
[abstract] [zulip topic] [slides] [video recording]
12:25 - 12:50 General automation in Coq through modular transformations Valentin Blot, Louise Dubois de Prisque, Chantal Keller and Pierre Vial
[abstract] [zulip topic] [slides] [video recording]
12:50 - 14:20Lunch break
14:20 - 15:00 Invited talk: Jasmin: Certified Workbench for High-Assurance and High-Speed Cryptography Vincent Laporte
[zulip topic] [slides] [video recording]
15:00 - 15:25 SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard and Bas Spitters
[abstract] [zulip topic] [slides] [video recording]
15:25 - 15:50 Extending MetaCoq Erasure: Extraction to Rust and Elm Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen and Bas Spitters
[abstract] [zulip topic] [slides] [video recording]
15:50 - 16:10Break
16:10 - 16:35 Certifying assembly optimizations in Coq by symbolic execution with hash-consing Léo Gourdin and Sylvain Boulmé
[abstract] [zulip topic] [slides] [video recording]
16:35 - 17:00 Coq/Ssreflect for large case-based graph theory proofs Ricardo Katz and Daniel Severin
[abstract] [zulip topic] [slides] [video recording]
17:00 - 17:30 Coq Development Team [slides] [video recording]

Important dates

Monday, May 3rd, 2021 (AoE)
Friday, May 7th, 2021 (AoE)
Deadline for submissions of talk proposals
Monday, May 31st, 2021
Notification to authors
Friday, July 2nd, 2021

Submission instructions

Authors should submit extended abstracts through EasyChair.

Relevant subject matter includes but is not limited to:

Submission Format

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.

Program Committee

Organization Contact

Christian Dozkal and Jean-Marie Madiot (

Past editions

See here.