# \[Call for Participation\] July 2nd: The Coq Workshop 2021

**URL:** <https://discourse.rocq-prover.org/t/call-for-participation-july-2nd-the-coq-workshop-2021/1362>\
**Category:** Announcements\
**Created:** [June 21, 2021, 3:07pm UTC](https://discourse.rocq-prover.org/t/call-for-participation-july-2nd-the-coq-workshop-2021/1362 "2021-06-21T15:07:29Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![chdoc](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/chdoc/32/552_2.png) [@chdoc](https://discourse.rocq-prover.org/u/chdoc)\
**Post date:** [June 21, 2021, 3:07pm UTC](https://discourse.rocq-prover.org/t/call-for-participation-july-2nd-the-coq-workshop-2021/1362/1 "2021-06-21T15:07:29Z")

</div>

## The Coq Workshop 2021: Call for Participation (July 2nd)

Colocated with the 12th conference on Interactive Theorem Proving (ITP 2021)  
Online

We are pleased to invite you to participate in the Coq workshop 2021, which will be held online on **July 2nd**. The Coq workshop is part of [ITP 2021](https://easyconferences.eu/itp2021/).

The Coq Workshop 2021 is the 12th iteration of the [Coq Workshop series](https://coq-workshop.gitlab.io/). The workshop brings together users, contributors, and developers of the [Coq proof assistant](https://coq.inria.fr/).

The Coq Workshop focuses on strengthening the [Coq community](https://coq.inria.fr/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 presentation and discussions, supplemented with invited talks.

# Program

### Invited talk:

Vincent Laporte. Jasmin: Certified Workbench for High-Assurance and High-Speed Cryptography

### Discussion session with the Coq development team

### Accepted talks:

- Reynald Affeldt and Cyril Cohen. _Formalization of the Lebesgue Measure in MathComp-Analysis_

- Reynald Affeldt, Xavier Allamigeon, Yves Bertot, Quentin Canu, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Laurent Théry and Anton Trunov. _Porting the Mathematical Components library to Hierarchy Builder_

- Cyril Cohen and Théo Zimmermann. _A Nix toolbox for reproducible Coq environments, Continuous Integration and artifact reuse_

- Johannes Hostert, Mark Koch and Dominik Kirst. _A Toolbox for Mechanised First-Order Logic_

- Frédéric Besson. _À la Nelson-Oppen Combination for congruence, lia and lra._

- Valentin Blot, Louise Dubois de Prisque, Chantal Keller and Pierre Vial. _General automation in Coq through modular transformations_

- Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard and Bas Spitters. _SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq_

- Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen and Bas Spitters. _Extending MetaCoq Erasure: Extraction to Rust and Elm_

- Léo Gourdin and Sylvain Boulmé. _Certifying assembly optimizations in Coq by symbolic execution with hash-consing_

- Ricardo Katz and Daniel Severin. _Coq/Ssreflect for large case-based graph theory proofs_

See [The Coq Workshop 2021](https://coq-workshop.gitlab.io/2021/) for the schedule.

# Registration:

See the ITP 2021 website for registration information:  
[Registration | ITP 2021](https://easyconferences.eu/itp2021/registration/)

## 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)

## Organisation contact (co-chairs):

Christian Doczkal and Jean-Marie Madiot ([coq2021@easychair.org](mailto:coq2021@easychair.org))