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
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
10:50 - 11:15 A Nix toolbox for reproducible Coq environments, Continuous Integration and artifact reuse Cyril Cohen and Théo Zimmermann
11:15 - 11:35Break
11:35 - 12:00 A Toolbox for Mechanised First-Order Logic Johannes Hostert, Mark Koch and Dominik Kirst
12:00 - 12:25 À la Nelson-Oppen Combination for congruence, lia and lra Frédéric Besson
12:25 - 12:50 General automation in Coq through modular transformations Valentin Blot, Louise Dubois de Prisque, Chantal Keller and Pierre Vial
12:50 - 14:20Lunch break
14:20 - 15:00 Invited talk: Jasmin: Certified Workbench for High-Assurance and High-Speed Cryptography Vincent Laporte
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
15:25 - 15:50 Extending MetaCoq Erasure: Extraction to Rust and Elm Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen and Bas Spitters
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é
16:35 - 17:00 Coq/Ssreflect for large case-based graph theory proofs Ricardo Katz and Daniel Severin
17:00 - 17:30 Coq Development Team

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.