coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Benjamin Pierce <bcpierce AT cis.upenn.edu>
- To: types-announce AT lists.seas.upenn.edu, coq-club AT inria.fr, Tej Chajed <tchajed AT mit.edu>
- Subject: [Coq-Club] CoqPL 2023, final program
- Date: Mon, 26 Dec 2022 17:00:00 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mail-vk1-f173.google.com
- Ironport-data: A9a23:Zr6h/auyq6jySAYnfjdmAiVewufnVJdaMUV32f8akzHdYApBsoF/q tZmKWjVPfaKMGKmftAlb4i0801T65PQndRhQQpvpHhmHi9EgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCY0idfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbyRFtcpvlDs15K6o4WlC4ARkDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJEhmEpIJ0M8mPWYUy fcfdzssQxqut9vjldpXSsE07igiBMziPYdapHI5iD+AUq1gTpfETKHHo9Rf2V/chOgURaeYN 5dfM2A2Kk2fOHWjOX9PYH46tO2jnnjyaTZVgEmYrLFx/nDeygo33bTwWDbQUozXHJ0Lxx7Gz o7A12LVWxE5a9ee8GaM40COpNPmuX7ZYp1HQdVU8dYz2AHJroAJMzUdUkL+qv2kgGalStdHI goV/DAvpO487iSWosLVWhS5pDuavUdZVYMPSKs17waCzqeS6AGcboQZctJfQNV2m9AnbxV76 ljTo9juWjdOnbe4eUvIo994sgiOESQSKGYDYwoNQg0E/8TvrekPYvTnHokL/Emd3o2dJN3g/ 9yZhHNh2OhL3Kbnw43+rA+X2Wv9znTcZldtvl2/Y46z0u9uiGeYi2GA7FHa6bNeL9/cQADe5 z4LnM+R6O1IBpaI/MBsfAnvNOH5jxpmGGeE6bKKI3XH32nyk5JEVd0BiAyS3G8zbq45lcbBO Sc/Qz956p5JJ2eNZqRqeY+3AMlC5fG+So69CaGINYAWM8EZmOq7EMdGNRH4M4fFwBhErE3DE crznTuEVydEV/w8kFJauc9MieFyrszB+Y8jbcmjk07PPUu2a3mSRrMIWGZinchohJ5oVD79q o4FX+PTk0s3eLSnPkH/rNBORXhXciBTLc6s96R/KLXYSiI4QzFJNhMk6el+E2CTt/8FyLmgE 7DUchMw9WcTclWeeFnUNSA5N+i0NXu9xFpiVRER0Z+T8yBLSe6SAG03LvPbpJF3pbwx/u0+V PQfZcSLD9JGTzmNqXxXboDwoMYmPF6njB6HdXjtKjUuXY9SdyqQ8P/dfyzr6HYvCAizvpAAu LGO7F7QbqcCYAVAN/zoTsyT4Wm/hlUno9IqbXD0eoFSXG7O7LlVLzfAi65rAsMUdjTG6Dio9 yeXJhY6p+D9hpI5wPPNj6XYsrWWKbJfH1VbLUbf/72ZJSnXxUv94I5iAcKjXyHRa3Pww4qmP d5q9vDbNOYWumpKv65XMadZ/Yhn6/TB/7ZlnxlZRlPVZFGVO5ZcC3ih3/gXkJZSx7Vc6DCEa mjW9vZ0Yby2ad7YSngPLw8Yb8OG5/Eeuh/Wyd8XeEzaxitGzICrYHVoHSunqXJideNuEYYf3 +0eltYc6FW/hjoUI9+2tH1o2FrWHEMQcZcMl888MNfwhxsJ22NyR8XWKhXL7aGlb/RONUgXI QGoupfSuoQE+G38dyscKHuc+8tcmpUEhz5SxnAgOVmiu4TIl9037jJr4BU1SQVelCtH2PMuY 2NECVB/JPiKzRdVhexofWOlKydeDjK3p23zzFookjXCbk+KD2biEkw0Cdyvzms4rV1OWyd9x 66J7lrlXRLBXtDD7gFrVWFL8/XcHMFMrCvck8WZLuG5NpgdYwu9pJSxZGAN+iDVMeloiGLp/ eBVrftNM4vlPistooo+OYmQ9ZIUbDumfGViY/VQzJklLFHmWgOZ+GaxchiqW8Z3Ofb131eyC JVuKuJxRh2O7nuygQ5BN5EcAY1fvaAP1IIZd6LJNFw2leKVjgBUvaL68gn8g24WQOtSr/stF 7OJdxy+PzyRoVB2h17yqNJ1PzvkQNscOyz58uOH0MQIMJMhrNBTdVoW4omumk7MNS5b9ACwu Q/dbfXa1N5ZlIZmxdPtNo5hBAyED8z5e8rV0QK0svVINcjuN+WXvSwri1DXBSZkFppPZMZSi pKMr8/R4EPJmJ0UQlLpscCNOIcR7PrjQdcNFNz8KUdruBerWeju0kMlwH+5I5kYq+FtzJCra CXgYfThaONPfclWwUBUTC1sExw9LaDTRYW4rAOfq8W8MDQs4TblHviGq0CwNXp6cxUWMaLQE gX34vaixu5JpbR2WSMrOatUPI9aEnTCB40WLtH/jGzNRC3gyFaPoaDrmhcc+CnGQCvMWtrz5 ZXeAAPyblKusaXP18tUqJF2ogZRNntmnO0sZQgIzraaUdxh4LIudozx8KnqC624VgT33ZD8I S/ONS4sUHqmGztDdhr47ZLoWQL36ini/DvmDmRBwq9WQ37e6EC87H9J7Spp+DFrYjblyqeqJ cx2FrjYIE2q2p8wLQoMzqXTvAqkr882AloD+Fu7jtT/BRBYDLkXvJCk8MyhSgSfe/zweI73y aTZiIyKrIxXiaI8LCq4R0NoJQ==
- Ironport-hdrordr: A9a23:ZLoJOa4PUxkTOI/sywPXwMXXdLJyesId70hD6qkRc20zTiX8ra qTdZsgpHzJYVoqOE3I+urgBEDjewK/yXcd2+B4VotKNzOW3VdAQrsSibcKAAeNJ8Q9zINgPG tbHJSWweefMWRH
- Ironport-phdr: A9a23:c9EYqB8ZpcnFB/9uWVC1ngc9DxPPW53KNwIYoqAql6hJOvz6uci4Y QqCtb400QOBdL6YwswHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yeC/94fTbghLizaxfLN/I RqrpgjNq8cahpdvJak2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3U bJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5 LpwRRT2lCkIKSI28GDPisxxkq1bpg6hpwdiyILQeY2ZKeZycr/Ycd4cWGFPXNteVzZZD4yzb 4UBAekPM/tGoYbhvFYBtweyCBO2Ce/z1jNFhHn71rA63eQ7FgHG2RQtEs8Qv3TSrtX6LqISU eGzzKLV1zvDbu1Z2S3h54fWbxsspuqDUq5occrQ10YvDR/KgUuLpIP5PjOVzf4Bs3WD7+V+U +KvjXQrpB9srTiy38ohjJTCiY0JxF7e7yp53Jo1KsOiSE59edOqEJteuiWUOoZ3Q84uX2Jlt iYmx7EYu5O2cykHxpQjyhPDZPGKboeF7gzgWeueIDp2hHJodbK/iRqs70Ss1uLyW8+p21hEq SpFl8PDtnEL1xHL8ciHS/R9/l+l2TmV0QDf8OZEIVo7lafdNpUvwaYwm4INvUjfGiL6gkb7g a+Mekk65OSk9v7rbqjkq5KSMYJ/lxvwPb40msOlBOQ1KggOUHaf+eS7zLDj+Ff2QLROjvEvj KnZs43WKd0VpqKkAQJY3Jwv6xm4Dzeh39QYmWcIIEhZdxKAiojlI1DOIPbmAvejm1mgjitny vTcMrDiApjBNGbPnKn8cbpn9kJRygQ+wcha551OC7EBJPzzWlX2tNzdFhI2KBC7w/7mCNpjz IMRRXyAD7SCMKzMq1CI/fgjI/SUZIALvjb9LeIp6ODzgn8kgVMde7Km0oMNaH+kBvRmP1mZY X30j9scCWsKpBYxTPT2iF2eVj5ef2q9X6Ul5j0iFI2mCZrDSZu2jbya3Ca7G4VWaXpcBlCNF 3fobYSEVO0WZCKcOM8y2gADAKSwU4I6kBiosgjnzbFqBu7V4TED84nu3cMz+vXekxd0+DBpS 4yW1HjIRGVplEsJQSU31eZxuwg19lqBmYN4iv5VGZQH+/hJWwU3ObbZzvA8BtzvDFHvZNCMH XyrRNevBDA3BuowzsUFbg4pEd66jx3Z1CeCCL4O0aGTCZoytK/Qwi6idI5G13/a2fx53BEdS cxVODjj3/Ynn+CyL4vAkkHD0r2vabxZxinGsmGK0WuJukhcFg92S6TMG34FNQPNtdqswETEQ ve1DKg/dBNbwJuIIbNLZ8figH1NReylJczTZWT3lmutVl6T3r3ZVIPxYC0G2TnFTk0NkgQd5 3GDYAI1HiasuWnTJCdjHEmpflvh9+84pX+mHQcv1w/fSUpn2vKu/wINw/yRT/RGxrUfpCIos Cl5Bn641tPSTsSD/k9vJfoHJ9w651hD2CTSsAkV0oWICadkixZedg12uxmrzBBrEsBalsNsq no2zQ10IKbe0VVbdjre04qicrvQYnL/+hyiccu0khnXzcqW96ET6f85t0SrvQenEVAn+mlm1 N8d2mWV55HDBg4fGZzrVUN/+x9/rrDcKi4zguGcnXdnKai5qDTP89koH6040humeZFSPL7FX A7+HssGBtS/ffQwkgvMDFpMN+RT+agoesK+IqHeiej7YaA6xmvg1Dscs+UfmgqW+iFxS/DFx cMAyvCchE6cUivkyU2muYbxkJxFYjcbGiy+zzLlDchffP4XH85DBGGwLsmw3tg7iYTqXisS/ lW7Bl4c08KBYhebdBrgxQBW0wIarWHtyk7ah3Rk1iokqKaSxnmEye/6dRcdMWNjT2h5y0r0L I6yyd0WQQL7Cmph3Avg7kH8ya9Boa15JGSGWkZEcR/9KGR6W7exvL6PCyJWwKshqj4fEOG1Y FTAD6X4vwNfySToWW1X2DE8cTiu/JT/hR1zzmyHfj5/q3/QeMc4whm6hpSUT/VJ3zccTyRQk jTeHR6hJ9Sv+5OZm4qLvu2lVm2nX4FeamGxldLG5Hb9vzczR0TgxLi6gbiFWUAi3DX+1sV2W CmAtxv6boTxluy7Pe9hYkh0FQr54st+FJt5l9hV5tlY0nwbi5OJuHsfxD2rYJMLhOSkNiNLH GFQkLu3qED/1UZuL2yE3df8X3SZmI56YsWiJ3kR0WQ75txLD6Gd6PpFmzF0qxy2t1G0A7A1k zEDxP8p8HNfjfsOvV9nxC6FA70IFkRwJiHljFKV9924quNaaHvlIt3SnAJu2MusCr2PuFQWU n3he5o4FiJY9ch2KxTRyHD17MfpdMSaPrdx/lWE1hzHieZSMpc4kPEH0DFmNWzKtnog0+cnj BZq0MLyrM2dJm5q5q78Hg9AO2i/eZYI4j+0x/U7/I7ez8W1E55mADlOQJb4UafiDmcJrfq+f weWTG9n9zHCSOKZR1PArh8h9S6HEoj3ZS/LYiNClpM7GkHbfAsG0WV2FH07hsJrSF7snZS7N h8/vndLvhb5skcelLwubUWuFDeH4l/vMG98SYDDfkUMqFgeoR6Ea4rGqbsjekMQtpy58F7Sd irCPVkOVSdRHRXaT1H7Yuv3vYmGqrfHQLr4d7yUOP2PsbAMDqjTg8v+js0+uW7Lb5vqXDEqD uVniBAbDDYpRoKAwWVJE2tOyGrMd5LJ/k7ivHAn6JnuqrKzH1u+rYqXV+kIaIspoUvnx/zZc bbX3XccS34QwJoIwTWgJKE3+lkUhmkucjCsFe5FrivRVOfKnaQRCRcHaiR1Pc8O7qQm3wALN 9SJwtXynqV1iPI4ETInHRToh92paMoWImq8KEKPBUCFM66DLCHKxMe/aL21SLlZhuFZ/xOqv jPTH0jmNzWF3z7nMnLneflLlz2eNQdCtZuVdx9sDS39T4ujZETka5l4ijo5xbByjXTPdCYdP TV6b0JRv+iQ4Cdf0ZAdUyRK6ntoK/XBmj7MtbGJbMZL96ExW2ItyLkJhRZyg6FY5yxFWvFvz S7br9o05kqjjvHK0D1sFhxHtjdMgouP+0RkI6TQsJdaChOmtFoA63udDxMSqp5rENrq7upaw cDOmbj4JR9Z/tvPu9YECs7Sbs+LLTByVHihUC6RFwYDQTOxYCvHgFdBlfiJ6nCPhp0zq5yph plXD7ECCwdzGfQdBUBoWtcFJd0kO1Fs2a7eh8kO632kqRDXT8gPpZHLWMWZBvD3ISqYh71JD /Pt6bj5NsIOLoD93QpvZkQoxOwi9GLLUNlW5DB5Ywky5khB7SonJoXS80fsawfo/nxKUPDtw UVwhQx5buAgsjzr5gVvTmc=
- Ironport-sdr: 63aa19ac_52/cBdSVPq0AXWIMLbYVLlCuJDZCGXXvcO+twj1JP8bdPYA 7i2gsAF70GC7Ff62kvVavCw6WDBrTTyO96MzjFg==
9th International Workshop on Coq for Programming Languages
Saturday, January 21, 2023, co-located with POPL
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)
- 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
- [Coq-Club] CoqPL 2023, final program, Benjamin Pierce, 12/26/2022
Archive powered by MHonArc 2.6.19+.