[TYPES/announce] [Call for Participation] July 2nd: The Coq Workshop 2021

[Christian Doczkal]

***********************************************************************
            The Coq Workshop 2021: Call for Participation
   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 https://coq-workshop.gitlab.io/2021/ for the schedule.


Registration:
- See the ITP 2021 website for registration information:
  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 at easychair.org)