The Ninth International Workshop on Coq for Programming LanguagesCoqPL 2023
The series of CoqPL workshops provide an opportunity for programming languages researchers and practitioners with an interest in Coq to meet and interact with one another and members from the core Coq development team. At the meeting, we will discuss upcoming new features, see talks and demonstrations of exciting current projects, solicit feedback for potential future changes to Coq itself, and generally work to strengthen the vibrant community around our favorite proof assistant.
Topics in scope include:
- Formalizations of PL research in Coq
- General purpose libraries and tactic language extensions
- Domain-specific libraries for programming language formalization and verification
- IDEs, profilers, tracers, debuggers, and testing tools
- Reports on ongoing proof efforts conducted via (or in the context of) the Coq proof assistant
- Experience reports from Coq usage in educational or industrial contexts
Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mTalk | Omnisemantics: Smooth Handling of Nondeterminism (Invited talk) CoqPL Samuel Gruetter Massachusetts Institute of Technology | ||
10:00 30mTalk | Interactive Theorem Proving in Logic Education：A Coq Formalization of ZFC Set Theory for Discrete Mathematics Teaching CoqPL File Attached | ||
11:00 - 12:30 | |||
11:00 30mTalk | Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation CoqPL File Attached | ||
11:30 30mTalk | Integrating graphical proofs in Coq CoqPL File Attached | ||
12:00 30mTalk | Towards Formally Verified Path ORAM in Coq CoqPL Hannah Leung University of Illinois Urbana-Champaign, Talia Ringer University of Illinois at Urbana-Champaign, Christopher W. Fletcher University of Illinois Urbana-Champaign File Attached | ||
14:00 - 15:30 | |||
14:00 30mTalk | Verified Differential Privacy for Finite Computers CoqPL Vivien Rindisbacher Boston University, Arthur Azevedo de Amorim Boston University, Marco Gaboardi Boston University File Attached | ||
14:30 30mTalk | Formalizing Monoidal Categories and Actions for Syntax with Binders CoqPL Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT (CNRS and Univ. of Toulouse), Kobe Wullaert Technical University Delft File Attached | ||
15:00 30mTalk | Certifying Complexity Analysis CoqPL Clément Aubert Augusta University, Thomas Rubiano LIPN – UMR 7030 Université Sorbonne Paris Nord, Neea Rusch Augusta University, Thomas Seiller CNRS File Attached | ||
16:00 - 17:30 | |||
16:00 45mTalk | Session with the Coq Development Team CoqPL | ||
Accepted Papers
Call for Presentations
To foster open discussion of cutting edge research which can later be published in full conference proceedings, we will not publish papers from the workshop. However, presentations may be recorded and the videos may be made publicly available.
Submission Details
Submission page: https://coqpl23.hotcrp.com/
Important Dates:
- Submission: Thursday, October 20, 2022
- Notification: Thursday, November 17, 2022
- Workshop: Saturday, January 21, 2023
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.
Danil Annenkov
Concordium
Denmark
Qinxiang Cao
Shanghai Jiao Tong University
China
Tej ChajedCo-chair
VMware Research
United States
Maxime Dénès
INRIA
Hugo Herbelin
Inria
Zoe Paraskevopoulou
Northeastern University
United States
Benjamin C. PierceCo-chair
University of Pennsylvania
United States
Clément Pit-Claudel
EPFL
Switzerland
Talia Ringer
University of Illinois at Urbana-Champaign
United States
Christine Rizkallah
University of Melbourne
Australia