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
You're viewing the program in a time zone which is different from your device's time zone change time zone

Sat 21 Jan

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

11:00 - 12:30
Session 2CoqPL at Scollay
11:00
30m
Talk
Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation
CoqPL
Dustin Jamner MIT CSAIL, Gabriel Kammer MIT, Adam Chlipala Massachusetts Institute of Technology
File Attached
11:30
30m
Talk
Integrating graphical proofs in Coq
CoqPL
Pablo Donato Ecole polytechnique, Benjamin Werner LIX, IPP, Kaustuv Chaudhuri INRIA & LIX, IPP
File Attached
12:00
30m
Talk
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
Session 3CoqPL at Scollay
14:00
30m
Talk
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
30m
Talk
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
30m
Talk
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
Session with the Coq development teamCoqPL at Scollay
16:00
45m
Talk
Session with the Coq Development Team
CoqPL

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.