The Coq Workshop 2020

Location: 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.

COVID-19 notice

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.

Important dates

April 13, 2020; April 27, 2020 May 1st, 2020 (AoE)
Deadline for abstract submission
April 29, 2020; May 20, 2020 May 25th, 2020
Notification to authors
July 5-6, 2020
Workshop

Participation instructions:

The workshop was held using Zoom; talks were streamed live on Youtube, and will be available soon.

The workshop was streamed using Youtube:

Workshop Chat Room:

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.

Diversity Chat Room:

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.

Program:

Bird's eye view

Time (Paris GMT+2) Sunday, July 5th, 2020 Monday, July 6th, 2020
10:00-10:20 Hierarchy Builder
10:20-10:40 A hierarchy of ordered types in Mathematical Components
10:40-11:00 Developing sequence and tree fintypes in MathComp
11:00-11:30 Break Break
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
12:30-13:00 Lunch
13:00-14:10 Lunch
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++
15:30-16:00 Break Break
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

Sunday July 5th, 2020

Panel: Libraries

Moderator: Bas Spitters

11:30-12:30
Panelists: [Zulip Discussion Room] [Slides]

Session: Meta-programming and automation

Chair: Matthieu Sozeau

14:30-14:50
FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs
Roberto Blanco, Matteo Manighetti and Dale Miller
[Zulip Discussion Room] [Abstract] [Slides]
14:50-15:10
Generating induction principles and subterm relations for inductive types using MetaCoq
Bohdan Liesnikov, Marcel Ullrich and Yannick Forster
[Zulip Discussion Room] [Abstract] [Slides]
15:10-15:30
A Decision Procedure for Equivalence Relations
Sébastien Michelland, Pierre Corbineau, Lionel Rieg and Karine Altisen
[Zulip Discussion Room] [Abstract] [Slides]

Session: Tools

Chair: Emilio J. Gallego Arias

16:00-16:20
The Coq Proof Script Visualiser (coq-psv)
Mario Frank
[Zulip Discussion Room] [Abstract] [Slides] [Examples]
16:20-16:40
A Gentle Introduction to Container-based CI for Coq projects
Érik Martin-Dorel
[Zulip Discussion Room] [Abstract] [Slides]
16:40-17:00
Learning to Format Coq Code Using Language Models
Pengyu Nie, Karl Palmskog, Junyi Jessy Li and Milos Gligoric
[Zulip Discussion Room] [Abstract] [Slides] [ArXiV]

Monday July 6th, 2020

Session: Mathematics

Chair: Yves Bertot

10:00-10:20
Hierarchy Builder
Cyril Cohen, Kazuhiko Sakaguchi and Enrico Tassi
[Zulip Discussion Room] [Abstract] [Slides]
10:20-10:40
A hierarchy of ordered types in Mathematical Components
Xavier Allamigeon, Cyril Cohen, Kazuhiko Sakaguchi and Pierre-Yves Strub
[Zulip Discussion Room] [Abstract] [Slides]
10:40-11:00
Developing sequence and tree fintypes in MathComp
Pierre-Léo Bégay, Pierre Crégut and Jean-Francois Monin
[Zulip Discussion Room] [Abstract] [Slides]

Invited talk

Chair: Hugo Herbelin

11:30-12:00
Invited talk: A Coq retrospective, at the heart of Coq architecture, the genesis of version 7.0
Jean-Christophe Filliâtre
[Zulip Discussion Room] [Slides] [Coq v7 Report]

Panel: Meeting with Coq Dev Team

Moderator: Matthieu Sozeau

12:00-13:00
With the presence of the Coq Team
[Zulip Discussion Room]

Session: Verification

Chair: François Pottier

14:10-14:30
Experience Report: Smuggling a Little Bit of Coq Inside a CAD Development Context
Dimitur Krustev
[Zulip Discussion Room] [Abstract] [Slides]
14:30-14:50
High-assurance field inversion for pairing-friendly primes
Benjamin S. Hvass, Diego F. Aranha and Bas Spitters
[Zulip Discussion Room] [Abstract] [Slides]
14:50-15:10
Verifying, testing and running smart contracts in ConCert
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen and Bas Spitters
[Zulip Discussion Room] [Abstract] [Slides]
15:10-15:30
Towards an Axiomatic Basis for C++
Gregory Malecha, Abhishek Anand and Gordon Stewart
[Zulip Discussion Room] [Abstract] [Slides]

Panel: Domain-agnostic and Domain-specific Proof Automation

Moderator: Arthur Charguéraud

16:00-17:00
Panelists: [Zulip Discussion Room]

Organization

Program committee

Organizers and co-chairs

Submission instructions

Authors should submit talk proposals through EasyChair.

Relevant subject matter includes but is not limited to:

Format

Extended abstract:

Past editions

See here.