The Eighth International Workshop on Coq for Programming LanguagesCoqPL 2022
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.
- 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
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.
- CoqPL 2021 in Copenhagen, Denmark (Virtual)
- CoqPL 2020 in New Orleans, LA, USA
- CoqPL 2019 in Cascais, Portugal
- CoqPL 2018 in Los Angeles, CA, USA
- CoqPL 2017 in Paris, France
- CoqPL 2016 in St Petersburg, FL, USA
- CoqPL 2015 in Mumbai, India
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00
|Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofsRemote|
I: Clément Pit-Claudel MIT / AWS
10:20 - 12:00
|A Visual Ltac Debugger in CoqIDERemote|
S: Jim Fehrle NoneFile Attached
|Scrap your boilerplate definitions in 10 lines of Ltac!InPerson|
|Tealeaves: Categorical structures for syntaxInPerson|
S: Lawrence Dunn University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Val Tannen University of Pennsylvania, USAFile Attached
|Towards a Formalization of Nominal Sets in CoqRemote|
|A Case for Lightweight Interfaces in CoqInPerson|
David Swasey BedRock Systems, Paolo G. Giarrusso BedRock Systems, S: Gregory Malecha BedRock SystemsFile Attached
13:30 - 14:30
|Verifying Concurrent, Crash-Safe Systems with PerennialRemote|
I: Joseph Tassarotti Boston College
14:30 - 14:50
|A Verified Pipeline from a Specification Language to Optimized, Safe RustRemote|
S: Rasmus Holdsbjerg-Larsen Aarhus University, Bas Spitters Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus UniversityPre-print File Attached
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.
Abstracts should be submitted via https://coqpl22.hotcrp.com/.