| CARVIEW |
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.
News
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.
Registration
To participate, please register for the workshops associated with ITP via Easy Conferences.Program
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:35 | Break |
| 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:20 | Lunch 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:10 | Break |
| 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
- Workshop
Submission instructions
Authors should submit extended abstracts through EasyChair.
Relevant subject matter includes but is not limited to:
- Theory and implementation of the Calculus of Inductive Constructions
- Language or tactic features
- Plugins and libraries for Coq
- Techniques for formalization programming languages and mathematics
- Applications and experience in education and industry
- Tools and platforms built on Coq (including interfaces)
- Formalization tricks and pearls
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
- Evelyne Contejean (CNRS, LRI)
- Christian Doczkal (INRIA) [chair]
- Amy Felty (University of Ottawa)
- Gaëtan Gilbert (INRIA)
- Ralf Jung (MPI-SWS)
- Marie Kerjean (CNRS, LIPN)
- Jean-Marie Madiot (INRIA) [chair]
- Kazuhiko Sakaguchi (University of Tsukuba)
- Kathrin Stark (Princeton University)
- Pierre-Yves Strub (École Polytechnique, LIX)
Organization Contact
Christian Dozkal and Jean-Marie Madiot (coq2021@easychair.org)