The Coq Workshop 2023

Affiliated with ITP 2023
Location: Białystok, Poland
Date: July 31, 2023

The Coq Workshop 2023 is the 14th 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.


Talks are 30 minutes long, plus 10 minutes for questions.

Time (Białystok, CEST - UTC+2) Monday, July 31, 2023
09:00 - 09:40 Environment-friendly monadic equational reasoning for OCaml Reynald Affeldt, Jacques Garrigue and Takafumi Saikawa
[abstract] [slides]
09:40 - 10:20 VSTlib: Library Components for Verified C Programs Andrew W. Appel
[abstract] [slides]
10:20 - 11:00 Formally verified source code optimization for safety critical software Wendlasida Ouedraogo, Danko Ilik and Lutz Straßburger
11:00 - 11:30Coffee break
11:30 - 12:10 Efficient, Extensional, and Generic Finite Maps in Coq-std++ Robbert Krebbers
[abstract] [slides]
12:10 - 12:50 A new Type-Class solver for Coq in Elpi Davide Fissore and Enrico Tassi
[abstract] [slides]
12:50 - 13:30 VLSM: A General Coq Framework for Reasoning About Faulty Distributed Systems Vlad Zamfir, Denisa Diaconescu, Wojciech Kołowski, Brandon Moore, Karl Palmskog, Traian Florin Serbanuta and Ioan Teodorescu
[abstract] [slides]
13:30 - 15:00Lunch break
15:00 - 15:40 (Co)datatypes via W-setoids and M-setoids Galaad Langlois, Damien Pous and Yannick Zakowski
[abstract] [slides]
15:40 - 16:20 Mathematics with Coq for first-year undergraduate students Pierre Rousselin
[abstract] [slides]
16:30 - 17:00Coffee break
17:00 - 18:00 Discussion with developers

Important dates

May 30, 2023 (AoE)
Deadline for submission of presentation proposals (Extended from May 26)
June 15, 2023
Notification to authors
July 31, 2023

Submission instructions

Authors should submit presentation proposals as extended abstracts through EasyChair.

Relevant subject matter includes but is not limited to:

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

Organizers and contact

Yves Bertot and Enrico Tassi (

Past editions

See here.