Colocated with the 12th conference on Interactive Theorem Proving (ITP 2021)
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.
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 presentation and discussions, supplemented with invited talks.
Vincent Laporte. Jasmin: Certified Workbench for High-Assurance and High-Speed Cryptography
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 for the schedule.
See the ITP 2021 website for registration information:
- 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)
Christian Doczkal and Jean-Marie Madiot (email@example.com)