Campus Condorcet, Aubervilliers (Paris region) online
Dates: July 5-6, 2020
New! Youtube streaming link!
New! Registration is open, and free!
New! Program added
The Coq Workshop 2020 is part of IJCAR 2020 and the Paris Nord Summer of LoVe 2020.
The Coq workshop 2020 is the 11th Coq Workshop. 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, supplemented with invited talks.
For the 35th birthday of the first release of Coq, this workshop will be spread over two days, and will include some panels in addition to the usual program.
Due to the COVID-19 outbreak and containment measures in France and in most other countries, the FSCD-IJCAR conferences to which the Coq workshop is affiliated will be held as a virtual event, and so will the Coq workshop.
Since the COVID-19 crisis is affecting everyone's life and since attending a virtual event requires less planning ahead than attending a physical one, we have extended the submission deadline.
The workshop was held using Zoom; talks were streamed live on Youtube, and will be available soon.
The workshop was streamed using Youtube:
Additionally, there will be a workshop-long chat room at Coq's main Zulip chat server. Zulip is an open source chat management software, "Slack-style". We have a specific "stream" for Workshop discussion, including general talk, coffee breaks, and individual threads for each talk to discuss and ask questions. Please see links to specific rooms in the program; topics start with a code denoting the day and talk number, for example [M3] denotes the 3rd regular talk on Monday, while [S2] denotes the 2nd talk on Sunday.
The workshop organizers acknowledge the diversity concerns in the Coq community. We have created a dedicated topic in our Zulip chat to discuss and propose diversity actions for the event, future events and more generally for the community. If you feel concerned by this topic, and especially if you are part of a minority, feel free to join the discussion even if you do not participate in the rest of the Coq Workshop.
|Time (Paris GMT+2)||Sunday, July 5th, 2020||Monday, July 6th, 2020|
|10:20-10:40||A hierarchy of ordered types in Mathematical Components|
|10:40-11:00||Developing sequence and tree fintypes in MathComp|
|11:30-12:00||Panel on Libraries||Invited talk: A Coq retrospective, at the heart of Coq architecture, the genesis of version 7.0|
|12:00-12:30||Coq Dev Team|
|14:10-14:30||Experience Report: Smuggling a Little Bit of Coq Inside a CAD Development Context|
|14:30-14:50||FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs||High-assurance field inversion for pairing-friendly primes|
|14:50-15:10||Generating induction principles and subterm relations for inductive types using MetaCoq||Verifying, testing and running smart contracts in ConCert|
|15:10-15:30||A Decision Procedure for Equivalence Relations||Towards an Axiomatic Basis for C++|
|16:00-16:20||The Coq Proof Script Visualiser (coq-psv)||Panel on automation|
|16:20-16:40||A Gentle Introduction to Container-based CI for Coq projects|
|16:40-17:00||Learning to Format Coq Code Using Language Models|
Moderator: Bas Spitters
Chair: Matthieu Sozeau
Chair: Emilio J. Gallego Arias
Chair: Yves Bertot
Chair: Hugo Herbelin
Moderator: Matthieu Sozeau
Chair: François Pottier
Moderator: Arthur Charguéraud
Authors should submit talk proposals through EasyChair.
Relevant subject matter includes but is not limited to: