coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] (2nd CfP) Dafny Workshop at POPL 2025

From: Stefan Zetzsche <stefanzetzsche AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] (2nd CfP) Dafny Workshop at POPL 2025
Date: Mon, 16 Sep 2024 15:20:55 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=stefanzetzsche AT gmail.com; spf=Pass smtp.mailfrom=stefanzetzsche AT gmail.com; spf=None smtp.helo=postmaster AT mail-pj1-f54.google.com
Ironport-data: A9a23:VGTKgK0+epHuxDTq6fbD5Ul1kn2cJEfYwER7XKvMYLTBsI5bpz0Cy zBNDD+EO/7fNmCkfIogOo6zo01TvsXVzdJkQAY63Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOHNIQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3Zhn8g1aYDkpOs/jf8EI24qyr0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJW3zuwNVkMFB1AaAJ1+lRWjt/q e0ACxlYO3hvh8ruqF66Yuxlh8BmNMuyeY1C5jdvyjbWCftgSpfGK0nIzYUAjXFg24YURKiYO pZxhTlHNHwsZzVUJloZAZQskfu6nXL/fhVXrVuUoew85G27IAlZgeaxYYuKIY3iqcN9lXiil 2nK3l7ABwACPti5yDPU8nOMmbqa9c/8cNlPTeXnp6ACbEeo7mcUEVgdUUaxieKoj1a3HdNZM U0dvCQ0xZXe72SuR9j5GgW6+TuK40JaVN1XHOk3rgqKz8I4/jp1GEADTD1hYuA39/MbVBEl8 ATTro/4HR9G5ej9pW2myp+Yqja7OC4wJGAEZDMZQQZt3zUFiNFj5v4oZoYzeJNZnuHI9SfML ydmRRXSap0WhM8Pkr25pBXJ3m7qqZ/OQQo4oA7QWwpJDz+Vhqb0PuRECnCCsp6sybp1qHHf5 hDofODAtogz4WmlznDlfQn0NOjBCwy5GDPdm0VzOJIq6i6g/XWuFagJv2sgeB00aJtbIGK5C KM2he+3zM8DVJdNRf8nC79d9+xznMAM6Py8CaCEMIUUOvCdiifdpXg2OBL4M5/RfLgEyvxmY cjKL65A/F4VDqNoyDf+RuEWl9cWKtMWlAvuqWTA503/i9K2PSbLIZ9caQfmRr5jsMus/l6Om /4BbJTi9vmqeLaiCsUh2dVOdQxiwLlSLcyelvG7gcbYelU2Qzl+VKK5LHFIU9UNopm5X9zgp hmVMnK0AnKl7ZEeAVzSMC4xW6ClRptls3MwMAolOFviiTBpYp+i4O1bP9E7dKUuvr4rh/Nlb eg3S+PZCNR2SxPD52s8a7v5p9dcbxiFv1+FEBekRzkdRKReYTL11OXqRSbR0RUfLzGWsJI+q oKw1wmATpskQR9jPfnsa/mu7g2QuCEdkd1tQ0DnJcl3R3S11qM3LSar3/k9DPwRGE+S2hqby AekLhMKrsbdo4IO0YfohILVi6yLAudBDk5hMG2D1omPNA7e5XiG7b5bdeS1IQDmS2L//Zu9a dVvz/3TNOMNmHBIudFeF4lH4L0f5dy1gZNn1SVhQWv2amq0BoNaInWp2ddFsotPzOR7vSq0Q ke+xclIC46WOc/KEE8jGyR9V76tjcorozj16eg5BG7Y5yUtpbqObhh0Dim20SdYKON4DZMhz eIfo/Up0g2YiCcxE9O4nytRpnWtLHsBbv0djaskIrTX0ygl9lITRqbnKH7SwIqOYNByIEUVM meqpK7dtY99mGvGUVQOTEbo48QMpK4gmh5wyH06G2+ogfvA3/8+4w1Q+284TyNT1RR27NhwM WlKaWxwKbm/wDNzoM1lQWqXOhpgASeB8Rfb0Go5l2z+TmipWFfSLWY7B/2/wUAB/09YfRlZ5 Lu9ylu5dRrPY+fKwXIUdWN+jv7sX/hd11fno9+2OdaBE70RQyvXsoX3aUUm8xLYUN4M3mvZr uxUzcNMQKzcNwtLhoYkCoOfhI8ieDrdKENsGfherb40R0fCczSP2B+LGUC7WuVJA9foqUaYK chfFvhjZiSE9hSlj24kXPYXArpOgvQWysIIeerrKU44orKvlGdVn6yKxBfupl0AYotIqtk8G LPzZjjZM223hFlooUHvgvRAGFKFZYgjWFWh8sGzqP4EBrASgtFKKEsS6Ia5j1+REQlg/i+Xg j/9Wr/r/7Rc7rpozqTREfRlJgSrKNnMevyC3yKtvv9vM97eE8f8mDkEi1vgPjYMZLsYZMtqp O7crP/2w0L3k7IkWE/Jm5S6Nvdo5OfjeMF1I87IPH1hsi/aY/DV4jwH4HGeFZNStcF0v+2Le lOdU9ShUvIwQPJf9W1xRwkFNChFEIXxTKPrhR3lnsS2EhJHjDD2doK2x0HmfURwV3EtKZbhL iTWpvz3xNRTjLoUNS8+H/s8XqNJeg7ya5AHKe/0myKTVFSzo1W4vbDnqxosxBfLBlSAE+f4+ Zj1fQf/RjvjpJD3yMxljKIqsi01FHpdhcwCTnAZ8fNyiBG4CzciBsYZOpMkFJpVs3LT0LfVW TLzV1YhWB7NBWl8TRbB4drdB1bVQqREP9riPTUm8n+Fcyr8VsvKHLJl8Twm+HtsPCfqyOa8M 9wF53nsJV6Lz4p0QfoIrOmO6Qu9Kig2GlpTkaw8ryDzP/raKbAD1XgkBAgUECKaT4fCk0LEI WVzTmdBKK1+pYgdDu44E0O52jlA1N8s89nsRSiKydfb/Y6cyYWsDdXhbvrr3ORrgNsifdYzq LCee4dJy2+T030X/6AuvrrFREOy5e2jRqCHEUMoeeHec2xcJIjq0wPuUBfjlP0fxTM=
Ironport-hdrordr: A9a23:MY8yDa2MJPtzCFofrkiM5AqjBL8kLtp133Aq2lEZdPU1SL3+qy nKpp4mPHDP+VUssR0b+exoW5PgfZq/z+8W3WB5B97LNzUO01HYSb2Kg7GSpwEI2BeTygee78 pdmmRFZ+EYxGIVsfrH
Ironport-phdr: A9a23:636tyxTYHTpKwPDfUS1D8THaA9psogOVAWYlg6HPa5pwe6iut67vI FbYra00ygOSBcOCu68P1LGempujcFJDyK7CikxKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizewb69+I A+roQjStsQajolvJ6gswRbVv3VEfPhbymxvKV+PhRjw4du+8oB++CpKofIh8MBAUaT+f6smS LFTESorPWMo6sD1rBfPVQSA6GcSXWUQiRpIHhPK7ArmUZfrsyv1rfRy1S+HNsDrV780WDCi7 6B2SB/0jSoMKjA0/H3LhsF2kalWpg+qqR5izI7OeIyaO/pwcK3ec90HW2ROQt1cWDZdDo6md YYDE/YNMOReooLgp1UOtxy+BQy0Ce3y1j9HmHH20rc80+88Eg7JwhAgHtMVsHvIrNX6KroZX OeuzKnU0zrDYelZ2TH86YfWbhAgoOqMUq5wccXP0kQvGAbFgU+RqYzhJT+ayuMNs22C4udmS OmghHIppRtrrTiz2scjlJPJhoQNx13K6Ch0xIY4K925RUN4fdOpEJRdui+VOoV2Rs4vTWFlt SI4x7AEpZK2eCcExYo5yxLBa/KKcJWE7Bz/WOuRLjl1gm9udry4hxa360egy+v8W9Gv0FZLo SpFit3MuWoL1xDJ7ciHUPR98l+h2TaIywDc9vtEIVgumaXHLJ4hx7g9nYcQv0TbBiL6hln6g auMekgn+uWk8frrbqjnq5OGN4J5hQfzObkwl8y7HOQ4KRQOUHaB+eqh1b3i/FP2Ta1WgvAwj 6LXqorVJd4Bqa68GwJV0pgs6xK4Dzq+1dQXh3gHLFZcdBKfjYjlJkjCIP74APqwmVisnzBrx /fJPr3lHJrBNGTMkLDkfbpl6k5czhQ8zcxH6p5KFr0MJOj/V0zxudDCEBM1Lg25z/znBdhyz o8eXHiAAq6dMKPcq1+I4ecvLvGXZI8Jpjn9JeIq5/jvjHAnhV8cfLKp0ocXaH+mBflmLECZb mDtgtcFC2sFog0+TOnyhF2ESjFcf2yyUL4k5jEnFIKmCp/OSp21jLybwCi7BoFWZnxBCl2UD XjocJyEV+4QZyKWP89uiScJVaOhSo8kzRGhrhX2y7thLurO+y0Xr4jv1NZv576bqRZn/jttS s+ZzmulTmdun2pOSSVl8rp4pBlG1lqN2K4wsfFEB8dY5/4BBhwmOJDVyf53F8LpUQLMVtiMQ VeiBN6hBGdiHZoK39YSbhMlSJ2ZhRfZ0n/ya1d0v7mCBZhvt7nZw2C0PMFljXDPyKgmiVAiB MpJL2yvwKBlpEDIH4CctUKfmu6xcLgEmjbX/TKY0WeAtUdKXRJiSq7FUFgQY0LXqZLy4UaRB 6S2B+EfOxBagdWHNrMMb9ToiVtcQ/K2I8jTbWu3iWqsFw2Dxr6kY4/jemFb1yLYWwAfiw5G2 3GAOEAlAzu55WLTCDs7DVX0f0bl6vVzslu+R04wihmINghviubz9RkSiviRDfgU29rooQ8Hr DN5VBa41tPSUJ+bohZ5Ob5beZU76UtG0mTQs0p8OIahJuZsnAxWdQM/pE7o2xhtb+cI2cE3s HMnyhZzIqOEwRtAcT2fx5X5JrzQLCH74hmub6fc3lyW3syR/+8D7/ExqlOruw/MdAJq6Glq3 dBTwXaA9I7BDAc6Xpf4U0Jx/B9/5vnbbiQ7+4LIxCh0K6Dn112Kk9ktBeYj1lOhZ4IFaPLCR FK0SZREQZXye4lI0xCzYxkJPf5f7vsxNsKiLL6d3bKzef1nhHSghHhG54Z01gSN8TB9Q6jGx cVgobnQ0w2ZWjP7lFrkvNrwnNUOfi0fEGO52yX4FpVaZqBacoMCCGPoKMqyjIYb5dalSztD+ VivCklTktS1dBSbaU7wwR9L3kQaiXOikCq8iTdzlnt6y8jXlDyLyOPkeh0dP2dNT2Q3llbgL 7+/iNUCVVSpZQwk/Pe8zX7z3LMT5KF2Lm2IBFxNYzCzNGZ6FK25qruFZcdLrpIuqyReFuqmM xiWTbv0oh1S1C2GfSMW3yw2eTisqJjljQdxiG+1I3N6rX6fcsZ1jRvS/93TQ/dN0yFOHnEpz 2mKQALlYZ/0oZ2djPKh+qimWnikV4FPfCWj1o6GuCahpCVrDRC5g/Gvi4jiGAk+3zX80ooiX iHJoRDgJ4jzgv7iYKQ3Iw8yXQG6tpYpf+M22pE9j5wRx3UA05Cc/H5c1Hz2Lc0ewqXmKnwEW T8MxdfRpgnjwkxqaHyTlOebHj2QxNVsY96ibyYYwCU4uopRFKqa5bpWkDdnuVG4oCreZPF8m nEWzv5kuxt4y6kZ/REgyCmQGOVYBlVVMyXqhRmU/cu1rKh/a2OmcLz2301714PEbvnKskRXX 3D3fY0nFCl745BkMV7C53b075ntZNjaad9A/g3RiRrLiPJZbY4gjvdfzzQyInrz5Dd2roxzx Qwrx5yxu5KLbnlg7L7sSAANLSX7PosS4m2/1vsYx5fOmdrzQdM5XW9XFJrwEaD2THRI7q+hb ljWVmV78yb+e/KXHBfDuhk46SuXSdbzcSnQfiFRzM0+FkfDYhYD0UZEBHNi2cRhXgGymJ6+K gEgunZItwS+8lwVmocKf1H+SjuN+1vuM21pDsDZdF0PsElD/xuHaJTOqLssQGcIuMXm9lXFK 3THNV0XVidQCxDCXxa7eeDwgLuIu+mAWrjkd6qIMejI8LYOEa/PnM3n05M6rWzVaIPSbj87X qd9gg0aDDh4A5iLwWxRDXZMxmSWNYjD407tn08/5ta29PChMO72za2IDbYacdBm+hTtxLyGK /bVnyFhbzBRypILw3bMjrkZxl8bzS90JXGrFvwbuCjBQbi1+OcfBgMHay51KMpD7r4tlghLN 8nBj9rp17l+xvcrAlZBXFbll4mnf8sPa226MVrGAg6MOtHkbXXTxNrrZKqnVbBKpOBdthn1o TTCVkG+YnKMkD7mUx3pOuZJzWmaMBFYpIChY0NtBGzkH7eEIlWwNN56iyFzwKVh3Cubcz5Bd 2IlLQUQ8u71j2sQmPh0Fm1f42AwKOCFn33c9OzEMtMNtuMtBC1oluVc6XB8yr1P7SgCSuYm/ Uma5tNovVyilfGCjzR9Vx8b4C1XiYyCu1dvJbfC/ZlNcXnB9RMJq26XDl5ZwrktQs2qoK1Wx tXVwejrLyxe9tvP4cYGL83dKcbCKHh4dBS0RHjbCwwKSTPtPmbazR848rna5jieqZ40rYLpk ZwFR+pAVVA7IfgdD1xsAN0IJJofttwMnruSjcpO7n27/kC5rCRyu5nGUreKA6yqJmvFy7ZDY BQMzPXzKoFBbuUTPmRtb1B7mMLBHE+CBbhw
Ironport-sdr: 66e83eed_pkLK9+NCu0kcTrUoxqmOHUlLIlJvgVsRlSpdLq10EkWaw/1 dwKLPGQeReHrRnJuyabzNwvj3Z4Kbb0t07jKvqw==

-----------------------------------------------------------------------------------------------------------------------------------
**
** Update: Program Committee, Keynote
**
-----------------------------------------------------------------------------------------------------------------------------------
**
** CALL FOR EXTENDED ABSTRACTS
**
** Dafny at POPL 2025
** 2nd Workshop on the Dafny Programming and Verification Language
** 19th of January 2025, Denver, Colorado, United States
**
** Submission Deadline:
** October 16, 2024
**
** https://popl25.sigplan.org/home/dafny-2025
** https://dafny25.hotcrp.com
**
-----------------------------------------------------------------------------------------------------------------------------------

Dafny is a verification-aware programming language that has native support for specifications
and proofs, and is equipped with an auto-active static program verifier. The workshop aims to
provide a platform for reports about applications of Dafny in industry, research on programming-
language concepts that are relevant to Dafny, and talks about Dafny’s role in teaching. Topics
include but are not limited to the following:

- Alternative verifier backends
- Coinduction and corecursion
- Comparison with other auto-active program verifiers (SPARK, F*, Why3, Viper, Whiley, …)
- Comparison with other proof assistants (Coq, Isabelle/HOL, Lean, …)
- Dafny in teaching
- Dynamic frames vs. separation logic vs. ownership
- Extensions and applications of Dafny
- Interactive theorem proving and SMT automation
- Logical foundations for Dafny (partial functions, nonempty types, extreme predicates, …)
- Program verification at industry-scale
- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and under-approximation, …
- Specification and proof inference for Dafny
- Test generation for Dafny
- Translation to or from Dafny and other languages

-----------------------------------------------------------------------------------------------------------------------------------
** IMPORTANT DATES
-----------------------------------------------------------------------------------------------------------------------------------

- Submission: Wednesday, October 16, 2024 (AoE)
- Notification: Wednesday, November 20, 2024
- Workshop: Sunday, January 19, 2025

-----------------------------------------------------------------------------------------------------------------------------------
** SUBMISSION GUIDELINES
-----------------------------------------------------------------------------------------------------------------------------------

To give a presentation at the workshop, please submit an anonymous extended abstract
(2-6 pages, excluding references) via hotcrp:

https://dafny25.hotcrp.com

Please use the acmart two-column sigplan sub-format LaTeX style to prepare
your submission:

https://www.sigplan.org/Resources/Author/

The workshop won’t have formal proceedings. However, presentations may be recorded and the

videos may be made publicly available. You are free to submit work for presentation that is or will

be published elsewhere.

-----------------------------------------------------------------------------------------------------------------------------------
** KEYNOTE
-----------------------------------------------------------------------------------------------------------------------------------

Nada Amin (Harvard University)

-----------------------------------------------------------------------------------------------------------------------------------
** ORGANISATION
-----------------------------------------------------------------------------------------------------------------------------------

Program Committee Chairs:
- Stefan Zetzsche (Amazon Web Services)

Program Committee:
- Seth Ahrenbach (Beneficial AI Foundation)
- Tej Chajed (University of Wisconsin–Madison)
- Alastair F. Donaldson (Imperial College London)
- Marie Farrell (The University of Manchester)
- Bryan Parno (Carnegie Mellon University)
- Clément Pit-Claudel (EPFL)

Steering Committee Chairs:
- Rustan Leino (Amazon Web Services)
- Joseph Tassarotti (New York University)
- Jean-Baptiste Tristan (Amazon Web Services)

-----------------------------------------------------------------------------------------------------------------------------------
** CONTACT
-----------------------------------------------------------------------------------------------------------------------------------

All questions about submission should be emailed to the program chair Stefan Zetzsche
(stefanze AT amazon.com).

[Coq-Club] (2nd CfP) Dafny Workshop at POPL 2025, Stefan Zetzsche, 09/16/2024