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.
Program
9:00-10:30
- 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
11:00-12:30
- 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
14:00-15:00
- 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
Registration
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.
Organization
Contact:
Syndicate