[TYPES/announce] CoqPL 2023, final program

[Benjamin Pierce]

CoqPL 2023 <https://urldefense.com/v3/__https://popl23.sigplan.org/home/CoqPL-2023__;!!IBzWLUs!TZh3NaebVwDJKGxnnPKNfcWPRMSzu_GM81aUIp2Vzf7Z5Zj76SSKWzH9-2w1MLJHOVOXobw81MOmzrWu8Gjf_-4nyyjGPmrQ3EI5$ >
9th International Workshop on Coq for Programming Languages
Saturday, January 21, 2023, co-located with POPL

The final CoqPL'23 program is now available
<https://urldefense.com/v3/__https://popl23.sigplan.org/home/CoqPL-2023*program__;Iw!!IBzWLUs!TZh3NaebVwDJKGxnnPKNfcWPRMSzu_GM81aUIp2Vzf7Z5Zj76SSKWzH9-2w1MLJHOVOXobw81MOmzrWu8Gjf_-4nyyjGPt_z2g-d$ >.  This year's edition
of CoqPL will consist of seven contributed talks and one invited talk.

*Workshop Overview*
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.

*Invited Talk*

   - *Omnisemantics: Smooth Handling of Nondeterminism* (Samuel Gruetter,
   MIT)

*Contributed Talks*

   - *Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving
   Compilation* (Dustin Jamner, Gabriel Kammer, and Adam Chlipala MIT)
   - *Verified Differential Privacy for Finite Computers* (Vivien
   Rindisbacher, Arthur Azevedo de Amorim, and Marco Gaboardi, Boston
   University)
   - *Integrating graphical proofs in Coq* (Pablo Donato, Ecole
   polytechnique, Benjamin Werner LIX, IPP, and Kaustuv Chaudhuri, INRIA &
   LIX, IPP)
   - *Interactive Theorem Proving in Logic Education：A Coq Formalization of
   ZFC Set Theory for Discrete Mathematics Teaching* (Xinyi Wan Shanghai
   and Qinxiang Cao, Shanghai Jiao Tong University)
   - *Formalizing Monoidal Categories and Actions for Syntax with Binders*
   (Benedikt Ahrens, TU Delft, Ralph Matthes IRIT, CNRS, and Univ. of
   Toulouse, and Kobe Wullaert, TU Delft)
   - *Certifying Complexity Analysis* (Clément Aubert, Augusta University,
   Thomas Rubiano LIPN, and Thomas Seiller, CNRS)
   - *Towards Formally Verified Path ORAM in Coq* (Hannah Leung, Talia
   Ringer, and Christopher W. Fletcher, University of Illinois
   Urbana-Champaign)

*Program Committee*

   - Danil Annenkov, Aarhus University, Denmark
   - Qinxiang Cao, Shanghai Jiao Tong University, China
   - Tej Chajed, VMware Research and University of Wisconsin, USA (co-chair)
   - Maxime Denes, INRIA, France
   - Hugo Herbelin, INRIA, France
   - Benjamin C. Pierce, University of Pennsylvania, USA (co-chair)
   - Clement Pit-Claudel, EPFL, Switzerland
   - Talia Ringer, University of Illinois, USA
   - Christine Rizkallah, University of Melbourne, Australia
   - Zoe Paraskevopoulou, Northeastern University, USA
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20221226/691b482b/attachment-0001.htm>