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.
Time (Białystok, CEST - UTC+2) | Monday, July 31, 2023 |
---|---|
09:00 - 09:40 |
Environment-friendly monadic equational reasoning for OCaml
[abstract] [slides] |
09:40 - 10:20 |
VSTlib: Library Components for Verified C Programs
[abstract] [slides] |
10:20 - 11:00 |
Formally verified source code optimization for safety critical software
[abstract] |
11:00 - 11:30 | Coffee break |
11:30 - 12:10 |
Efficient, Extensional, and Generic Finite Maps in Coq-std++
[abstract] [slides] |
12:10 - 12:50 |
A new Type-Class solver for Coq in Elpi
[abstract] [slides] |
12:50 - 13:30 |
VLSM: A General Coq Framework for Reasoning About Faulty Distributed Systems
[abstract] [slides] |
13:30 - 15:00 | Lunch break |
15:00 - 15:40 |
(Co)datatypes via W-setoids and M-setoids
[abstract] [slides] |
15:40 - 16:20 |
Mathematics with Coq for first-year undergraduate students
[abstract] [slides] |
16:30 - 17:00 | Coffee break |
17:00 - 18:00 | Discussion with developers |
Authors should submit presentation proposals as extended abstracts through EasyChair.
Relevant subject matter includes but is not limited to:
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.
Yves Bertot and Enrico Tassi (coq2023@easychair.org)