<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p>
    </p>
    <div class="moz-text-flowed" style="font-family: -moz-fixed;
      font-size: 12px;" lang="x-unicode">We are pleased to invite you to
      submit presentation proposals for the Coq Workshop 2023, which
      will be held in Białystok, Poland on July 31, 2023, as a satellite
      to the ITP conference.
      <br>
      <br>
      <a class="moz-txt-link-freetext" href="https://urldefense.com/v3/__https://coq-workshop.gitlab.io/2023/__;!!IBzWLUs!X_sYFMo_a1qe2a9T3xFecgAioGJwsNC2QtmKfb5RsuE0_sGgs3pl33kApYuOGqAAiph_VR8s9U2jYpMu-rGMwxDwaBYP0a8rugpA$">https://coq-workshop.gitlab.io/2023/</a>
      <br>
      <br>
      <br>
      The Coq Workshop 2023 is the 14th installment of the Coq Workshop
      series. The workshop brings together users, contributors, and
      developers of the Coq proof assistant.
      <br>
      <br>
      The Coq Workshop focuses on strengthening the Coq community and
      providing a forum for discussing practical issues, including the
      future of the Coq software, piece of software based on type theory
      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.
      <br>
      <br>
      <br>
      Important dates:
      <br>
      <br>
          May 26, 2023 (AoE): Deadline for submission of presentation
      proposals
      <br>
          June 15, 2023: Notification to authors
      <br>
          July 31, 2023: Workshop
      <br>
      <br>
      Submission instructions:
      <br>
      <br>
      Authors should submit presentation proposals as extended abstracts
      <br>
      through EasyChair.
      <br>
      <br>
      Relevant subject matter includes but is not limited to:
      <br>
      <br>
          Language or tactic features for Coq
      <br>
          Theory and implementation of the Calculus of Inductive
      Constructions
      <br>
          Applications of Coq and experience reports on Coq use in
      education and
      <br>
               industry
      <br>
          Tools and platforms built on Coq
      <br>
          Plugins and libraries for Coq
      <br>
          Interfacing with Coq
      <br>
          Formalization tricks and Coq pearls
      <br>
      <br>
      Submission format:
      <br>
      <br>
      Presentation proposals should be no more than 2 pages in length
      <br>
      including bibliographic references, and should use the EasyChair
      style
      <br>
      with the fullpage package. All submissions must be in PDF format.
      <br>
      <br>
      Program committee:
      <br>
      <br>
          Nada Amin (Harvard)
      <br>
          Jesper Bengtson (IT-University of Copenhagen)
      <br>
          Yves Bertot (Inria) [chair]
      <br>
          Ana Borges (University of Barcelona)
      <br>
          Chantal Keller (LMF, Université Paris-Saclay)
      <br>
          Pierre Roux (ONERA, Toulouse)
      <br>
          Takafumi Saikawa (Nagoya University)
      <br>
          Enrico Tassi (Inria) [chair]
      <br>
      <br>
      Organizers and contact:
      <br>
      <br>
      Enrico Tassi and Yves Bertot (<a class="moz-txt-link-abbreviated
        moz-txt-link-freetext" href="mailto:coq2023@easychair.org">coq2023@easychair.org</a>)
      <br>
      <br>
    </div>
  </body>
</html>