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.
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
- 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
Videos on YouTube
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | |||
09:00 60mKeynote | Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofsRemote CoqPL | ||
10:20 - 12:00 | |||
10:20 20mTalk | A Visual Ltac Debugger in CoqIDERemote CoqPL File Attached | ||
10:40 20mTalk | Scrap your boilerplate definitions in 10 lines of Ltac!InPerson CoqPL File Attached | ||
11:00 20mTalk | 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 20mTalk | Towards a Formalization of Nominal Sets in CoqRemote CoqPL File Attached | ||
11:40 20mTalk | 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 | |||
13:30 60mKeynote | Verifying Concurrent, Crash-Safe Systems with PerennialRemote CoqPL | ||
14:30 - 14:50 | |||
14:30 20mTalk | 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 | |||
15:05 45mPanel | 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 | ||
Accepted Papers
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.
| Sat 22 Jan 2022 Workshop |
| Thu 18 Nov 2021 Author Notification |
| Thu 21 Oct 2021 Abstract Submission |
Abhishek Anand
Cornell University
United States
Lourdes del Carmen González-Huesca
National Autonomous University of Mexico
Mexico
Jason Gross
MIT CSAIL
United States
Chung-Kil Hur
Seoul National University
South Korea
Leonidas Lampropoulos
University of Maryland, College Park
Greece
Xavier Leroy
Collège de France
France
Enrico Tassi
INRIA
France