The Coq Workshop 2022

Affiliated with ITP 2022, part of FLoC 2022
Location: Haifa, Israel
Date: August 12, 2022

The Coq Workshop 2022 is the 13th installment of the Coq Workshop series. The workshop brings together developers, contributors, and users of the Coq proof assistant. 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, rather than serving as a venue for traditional research papers, the workshop is organized around informal presentations and discussions.

Program

Talks will be 22 minutes long + up to 8 minutes for questions. See also the program on EasyChair.

Invited talk: Emilio Jesús Gallego Arias and Shachar Itzhaky: jsCoq: Literate Proof Documents Dressed for the Web

Time (Haifa, GMT+3)	Friday, August 12, 2022
09:30 - 10:00	A Coq Library for Mechanised First-Order Logic Dominik Kirst, Johannes Hostert, Andrej Dudenhefner, Yannick Forster, Marc Hermes, Mark Koch, Dominique Larchey-Wendling, Niklas Mück, Benjamin Peters, Gert Smolka and Dominik Wehr [abstract] [slides] [code]
10:00 - 10:30	QuantumLib: A Library for Quantum Computing in Coq Jacob Zweifler, Kesha Hietala and Robert Rand [abstract] [slides] [code]
10:30 - 11:00	Coffee break
11:00 - 11:30	Trakt: a generic pre-processing tactic for theory-based proof automation Denis Cousineau, Enzo Crance and Assia Mahboubi [abstract] [slides] [video] [zulip stream] [code]
11:30 - 12:00	10 Years of Superlinear Slowness in Coq Jason Gross and Andres Erbsen [abstract] [slides] [video]
12:00 - 12:30	Autogenerating Natural Language Proofs for Proof Education Seth Poulsen, Matthew West and Talia Ringer [abstract] [slides] [video] [code]
12:30 - 14:00	Lunch break
14:00 - 15:00	jsCoq: Literate Proof Documents Dressed for the Web Emilio Jesús Gallego Arias and Shachar Itzhaky [code]
15:00 - 15:30	HenBlocks: Structured Editing for Coq Bernard Boey and Michael D. Adams [abstract] [slides] [code]
15:30 - 16:00	Coffee break
16:00 - 16:30	Coq Community Survey 2022: Summary of Results Ana de Almeida Borges, Jean-Rémy Falleri, Jim Fehrle, Emilio Jesús Gallego Arias, Erik Martin-Dorel, Karl Palmskog, Alexander Serebrenik and Théo Zimmermann [abstract] [slides] [blogpost 1] [blogpost 2] [blogpost 3]
16:30 - 17:00	Discussion with Coq Core Development Team Emilio Jesús Gallego Arias and Jason Gross

Important dates

May 10, 2022 (AoE): Deadline for submission of presentation proposals
June 10, 2022: Notification to authors
August 12, 2022: Workshop

Submission instructions

Authors should submit presentation proposals as extended abstracts through EasyChair.

Relevant subject matter includes but is not limited to:

Language or tactic features for Coq
Theory and implementation of the Calculus of Inductive Constructions
Applications of Coq and experience reports on Coq use in education and industry
Tools and platforms built on Coq
Plugins and libraries for Coq
Interfacing with Coq
Formalization tricks and Coq pearls

Submission format

Presentation proposals should be no more than 2 pages in length including bibliographic references, and should use the EasyChair style with the fullpage package. All submissions must be in PDF format.

Program committee

Łukasz Czajka (Technical University of Dortmund)
Emily First (University of Massachusetts Amherst)
Kesha Hietala (University of Maryland)
Shachar Itzhaky (Technion)
Xavier Leroy (Collège de France and Inria)
Érik Martin-Dorel (IRIT)
Anders Mörtberg (Stockholm University)
Karl Palmskog (KTH Royal Institute of Technology) [chair]
Clément Pit-Claudel (Amazon AWS)
Vincent Rahli (University of Birmingham)
Talia Ringer (University of Illinois at Urbana-Champaign) [chair]

Organizers and contact

Karl Palmskog and Talia Ringer (coq2022@easychair.org)

Past editions

See here.