The CoqPL workshop series is an opportunity for programming languages researchers to meet and interact with one another and with members from the core Coq development team. We will discuss upcoming new features, see talks and demonstrations of exciting current projects, solicit feedback for potential future changes, and work to strengthen the vibrant community around our favorite proof assistant.

Topics in Scope

  • Formalizations of PL research in Coq
  • Experience reports from Coq users in research, education, and industry
  • General-purpose libraries and tactic language extensions
  • Domain-specific libraries for programming language formalization and verification
  • IDEs, profilers, tracers, debuggers, and testing tools

Workshop Format

The workshop format will be driven by you, members of the community. We will solicit abstracts for talks and proposals for demonstrations and flesh out format details based on responses. We expect the final program to include experiment reports, panel discussions, and invited talks (details TBA). Talks will be selected according to relevance to the workshop, based on the submission of an extended abstract.

To foster open discussion of cutting-edge research that can later be published in full conference proceedings, we will not publish papers from the workshop. However, presentations will be recorded and the videos made publicly available.

Previous Workshop Editions

This program is tentative and subject to change.

You're viewing the program in a time zone which is different from your device's time zone - change time zone

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Invited Talk ICoqPL at Salon I
Chair(s): Benjamin C. Pierce University of Pennsylvania
09:00
60m
Keynote
Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofsRemote
CoqPL
10:20 - 12:00
Contributed Talks (Morning)CoqPL at Salon I
Chair(s): Benjamin C. Pierce University of Pennsylvania
10:20
20m
Talk
A Visual Ltac Debugger in CoqIDERemote
CoqPL
S: Jim Fehrle None
File Attached
10:40
20m
Talk
Scrap your boilerplate definitions in 10 lines of Ltac!InPerson
CoqPL
S: Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
File Attached
11:00
20m
Talk
Tealeaves: Categorical structures for syntaxInPerson
CoqPL
S: Lawrence Dunn University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Val Tannen University of Pennsylvania, USA
File Attached
11:20
20m
Talk
Towards a Formalization of Nominal Sets in CoqRemote
CoqPL
S: Fabrício S. Paranhos Universidade Federal de Goiás, Daniel Ventura Universidade Federal de Goiás
File Attached
11:40
20m
Talk
A Case for Lightweight Interfaces in CoqInPerson
CoqPL
David Swasey BedRock Systems, Paolo G. Giarrusso BedRock Systems, S: Gregory Malecha BedRock Systems
File Attached
13:30 - 14:30
Invited Talk IICoqPL at Salon I
Chair(s): Amin Timany Aarhus University
13:30
60m
Keynote
Verifying Concurrent, Crash-Safe Systems with PerennialRemote
CoqPL
I: Joseph Tassarotti Boston College
14:30 - 14:50
Contributed Talk (Afternoon)CoqPL at Salon I
Chair(s): Amin Timany Aarhus University
14:30
20m
Talk
A Verified Pipeline from a Specification Language to Optimized, Safe RustRemote
CoqPL
S: Rasmus Holdsbjerg-Larsen Aarhus University, Bas Spitters Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University
Pre-print File Attached
15:05 - 15:50
Session with the Coq Development TeamCoqPL at Salon I
Chair(s): Amin Timany Aarhus University
15:05
45m
Panel
Session with the Coq Development TeamRemote
CoqPL
S: Matthieu Sozeau Inria, S: Yves Bertot INRIA, S: Hugo Herbelin , S: Emilio Jesús Gallego Arias INRIA, S: Jason Gross MIT CSAIL
Hide past events

Submissions

Submissions for talks and demonstrations should be described in an extended abstract, between 1 and 2 pages in length (excluding bibliography). We suggest formatting the text using the two-column ACM SIGPLAN latex style (9pt font). Templates are available from the ACM SIGPLAN page: http://www.sigplan.org/Resources/Author.

Submission site

Abstracts should be submitted via https://coqpl22.hotcrp.com/.

Contact

For any queries, please contact Benjamin Pierce or Amin Timany.