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

Announcements
1

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.

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 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 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@easychair.org)

1 Like