The Coq workshop 2015

The 7th Coq Workshop
Sophia Antipolis, France
June 26, 2015

The Coq Workshop series brings together Coq users, developers, and contributors.

While conferences usually provide a venue for traditional research papers, 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, the workshop will be organized around informal presentations and discussions.

The seventh Coq workshop happens at the end of the first Coq Coding Sprint.



  • Category Theory in Coq 8.5
    Amin Timany and Bart Jacobs (abstract)
  • Adventures in the (not so) Complex Space
    Emilio Jesús Gallego Arias and Pierre Jouvelot (abstract)
  • How to express convergence for analysis in Coq
    Catherine Lelay (abstract)

10:30-11:00, Coffee break


  • Finitary-based Domain Theory in Coq: An Early Report
    Moez Abdelgawad (abstract)
  • Gradual Certified Programming in Coq
    Éric Tanter and Nicolas Tabareau (full paper)
  • A ROS (Robot Operating System) shim for Coq
    Abhishek Anand (abstract)

12:30-14:00, Lunch break


  • Toward Nitpick and Sledgehammer for Coq
    Jasmin Christian Blanchette (abstract)
  • Coqoon/PIDE : Asynchronous Coq proof development in Eclipse
    Alexander Faithfull and Jesper Bengtson (abstract)

15:00-15:30, Coffee Break

15:30-18:00, General discussion

  • News from the Coq development
  • Demonstrations
  • Topics addressed during the Coq coding sprint

Important dates

  • June 15, 2015 Deadline for registration
  • June 26, 2015 Workshop date


Thanks to the support of Inria, participation to this workshop is free (but no meals are included), but registration is mandatory. The registration form is available at the following address.

Local information

Follow this link for information on how to get to the workshop's location and this link for information about accommodation and nearby hotels.

Call for presentations (closed)

The call for presentation and the program committee are described in the following page.