<div dir="ltr"><div style="text-align:center"><font size="4"><a href="https://urldefense.com/v3/__https://popl23.sigplan.org/home/CoqPL-2023__;!!IBzWLUs!TZh3NaebVwDJKGxnnPKNfcWPRMSzu_GM81aUIp2Vzf7Z5Zj76SSKWzH9-2w1MLJHOVOXobw81MOmzrWu8Gjf_-4nyyjGPmrQ3EI5$" target="_blank">CoqPL 2023</a></font></div><div style="text-align:center">9th International Workshop on Coq for Programming Languages</div><div style="text-align:center">Saturday, January 21, 2023, co-located with POPL</div><div style="text-align:center"><br></div>The final CoqPL'23 program is <a href="https://urldefense.com/v3/__https://popl23.sigplan.org/home/CoqPL-2023*program__;Iw!!IBzWLUs!TZh3NaebVwDJKGxnnPKNfcWPRMSzu_GM81aUIp2Vzf7Z5Zj76SSKWzH9-2w1MLJHOVOXobw81MOmzrWu8Gjf_-4nyyjGPt_z2g-d$" target="_blank">now available</a>.  This year's edition of CoqPL will consist of seven contributed talks and one invited talk.<br><br><b>Workshop Overview</b><br>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.<br><br><b>Invited Talk</b><br><ul><li><i>Omnisemantics: Smooth Handling of Nondeterminism</i> (Samuel Gruetter, MIT)</li></ul><b>Contributed Talks</b><br><ul><li><i>Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation</i> (Dustin Jamner, Gabriel Kammer, and Adam Chlipala MIT)</li><li><i>Verified Differential Privacy for Finite Computers</i> (Vivien Rindisbacher, Arthur Azevedo de Amorim, and Marco Gaboardi, Boston University)<br></li><li><i>Integrating graphical proofs in Coq</i> (Pablo Donato, Ecole polytechnique, Benjamin Werner LIX, IPP, and Kaustuv Chaudhuri, INRIA & LIX, IPP)<br></li><li><i>Interactive Theorem Proving in Logic Education：A Coq Formalization of ZFC Set Theory for Discrete Mathematics Teaching</i> (Xinyi Wan Shanghai and Qinxiang Cao, Shanghai Jiao Tong University)<br></li><li><i>Formalizing Monoidal Categories and Actions for Syntax with Binders</i> (Benedikt Ahrens, TU Delft, Ralph Matthes IRIT, CNRS, and Univ. of Toulouse, and Kobe Wullaert, TU Delft)<br></li><li><i>Certifying Complexity Analysis</i> (Clément Aubert, Augusta University, Thomas Rubiano LIPN, and Thomas Seiller, CNRS)<br></li><li><i>Towards Formally Verified Path ORAM in Coq</i> (Hannah Leung, Talia Ringer, and Christopher W. Fletcher, University of Illinois Urbana-Champaign)<br></li></ul><div><b>Program Committee</b><br><ul><li>Danil Annenkov, Aarhus University, Denmark<br></li><li>Qinxiang Cao, Shanghai Jiao Tong University, China<br></li><li>Tej Chajed, VMware Research and University of Wisconsin, USA (co-chair)<br></li><li>Maxime Denes, INRIA, France<br></li><li>Hugo Herbelin, INRIA, France<br></li><li>Benjamin C. Pierce, University of Pennsylvania, USA (co-chair)<br></li><li>Clement Pit-Claudel, EPFL, Switzerland<br></li><li>Talia Ringer, University of Illinois, USA<br></li><li>Christine Rizkallah, University of Melbourne, Australia<br></li><li>Zoe Paraskevopoulou, Northeastern University, USA<br></li></ul><div><br></div></div></div>