coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Stefan <stefanzetzsche AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Workshop on Dafny at POPL 24 (Call for Papers)
- Date: Thu, 31 Aug 2023 12:02:50 +0100
- Authentication-results: mail2-smtp-roc.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-wr1-f45.google.com
- Ironport-data: A9a23:J75IMKg7ZrV58eB850x3gFzgX161CRUKZh0ujC45NGQN5FlHY01je htvUGqOM/2KZzb9L40jYI6/80JUvZSHyddgSFdrr3o2Ey5jpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqieUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYqdDpOg06/gEk35q+q6GhB5gVWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGKgYdM6Ad2+tNK3xI8 /81DRI8azuqmLfjqF67YrEEasULKcDqOMYAoCglw22ES/khRp/HTuPB4towMDUY3JgfW6aDI ZBDMHwzMXwsYDUXUrsTIIkikemhgGvyby9Do1KYjaUy6mnXigd21dABNfKMIIfUG5kIzh/wS mTu+1nBIkBZFuCm1HnCqSu0hu+XoRzcYddHfFG/3rsw6LGJ/UQYDwRTXl+mq9Gim0umUpReL VYV82wgt8APGFeDS9D8W1inuifBsEJBHdVXFOI+5UeGza+8DxulO1XohwVpMLQO3PLajxRzv rNQt4KyXW5co/eORGiD97yZizq3NGJHZSUBfCIIB09NqdXqvIh53FqFQ8dBAZyFqIT/OQjx5 DSW8wk4pbEY1vAQ24uBoFvovjOLp7rydDAT2Dn5ZGyf015GVNaXXLDwsVn/xtRcHbmdVWiE7 SQlmdDBzeUgDqOttS2qQccLFo6H//yubT/W2wZuO7ID9D2d3WGpUq4NwTN5JWZvat0lfx2wa mDtmAph3r1hF1r0Ur1WOqWaFNYP4ZX7M+jcRtT4T4Zrc4dgUg2q5wRsbhOg5H/sm00Sjq0PA 5eXXsKyB3I8C6487j6Ja8oC8L0s1AYs7HjyQM3l8hGZzrauXn6ZZrMbOl+obOpizqeloh3Qw ulPJfmx1BRTf+3vUBb5qbdJAwgxEkE6IpTqp+h8VO2JeFNmEV58Lc7h++oqfog9kplFkuvNw GqGZXZZ71jB1FnnMgSBb05xZIz/BahfqW0JBg1yHFKK9UV6X6ORwvY+TaYnRZgm6+1p8tBsR dYnZcirI6pCWxbHyRsnfLj/q41oSzqzjynXZCGnTSQNfac5YwnF5NW+chDdz3QMBHDvtO8Vg b6p5iXES7UtGiVgC8f3bqq07lWT5HIypsN7b3HqEPJyJnr+1ZdMKjPgqMM3L+UnCwTx9hHD2 ym4WR4n9PTw+akr+9z3tIW4hoaOEdomOHFFHmPevI2EBQOD8kWNmYZ/Afu1JxbDX2bJ+YKnV +Vf79f4FNYlxF9qkY5NI4xH/JIExenEhuFll1x/PXDxcV6UJKtqISCG0elxp6R9/OJlljXsa H2f2OtxGOuvCJv+HU8zNTgVSL2J9csplwn46dU3J0TH5xFLwoeXbHUKPzSxjH1yEbgkFqIk3 uYrh+AO4SOdlBcBE4iLnwJUxUu2P10CVKQV7MgaCbD0lztxm01jYIPdOADy8pqge9VBCWh0A z621Y7ppaVQ+VrGSFU3TUPy5Ot6gY8fnixF13oQDg2ttuedo8QozTp91C8STDVF6jlmiMVNY nNKMW9xLoWwpwZYvtBJBT2QKlsQFS+n9VzU4HpXsX/SUG2DdHHHdU85MsazpHEpyXpWJGVnz evJ2VTecGjYee/q1XEPQm9jkfvoSOJx+iDkmMyKG8ekHYEwUQH6g52BNHY5lB/6Pfwf3EH3h /Fm3OJVW53JMSQ9p64aCY7D24pJGVrAbCZHTOp69awEIXDEdXvgkXKSIkS2YYVWK+aM7Ua8D Nd0K9lSUwilkhyDtS0fGbVGNooccCTFPzbeUuiDya86X7qjQv5BtZvR8m3hnjZuTYkz18k6L YzVenSJFWn4ab64XYPShJEsB4Z6SYBsiM7AMCSd/+AAFpZFu+ZpGa33+qXhpG2baWOL4DrN1 D4upMbqIyhKxoFlno+qGaJGb+lxxRUfS8zQmD2OXx9ygR8j/CsAW875arUqAuiOAYYsZg==
- Ironport-hdrordr: A9a23:Ji1Ap6s9Her4nv7ijoxJiY5n7skDTdV00zEX/kB9WHVpm62j5q KTdZEgvyMc5wxhPk3I9erwW5VoP0mskqKdkLNhWItKNTOO0ADJEGgL1+rfKlbbaknDH4BmpN 5dmmtFZOEYz2IWsS832maF+q4bsaG6GWmT69vj8w==
- Ironport-phdr: A9a23:bN0RrxOLRWrtpxrBTsYl6nbKBxdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv6sr1QORFt6Bo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6z9pHJfglFiyaxbbx8I RmosA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S 6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5 KlpVRDokj8KOT4l/27Yl8J+j6xVrgymqRFk2YHYfISVOeB+fq/Bf94XQ3dKUMZLVyxGB4Oxd 5YBD/YfMuZWtYb9oUYFoBylBQmwGuzvxCVHhnn33KIkz+QgEBrG0xAgH90Qq3nUo9D1O70TU eCx1qXH0TLDb/ZP1Dr79YPHfQwvr+uWUrJsbcre11MvFwXdg1iQqYHrMC+Z2+cQvmWV8+ZsS OyihWAppQxvrTaixNohh4rUio4Iyl3J6SV3zYI7KNO4SEN2fNypHYdQuSyZNoZ7RN4pTW9vu CY/0LIGuJi7cTARyJQmyB7fc/iHfJKO4h75U+aROzh4iGpleLK4mxa97VKgyvXmWsao11ZKq yxImcTPuHAVzxHf9NSLR/9n8kqi2TuDzR7f5v9ZLUwumqfWK4Ytz7w0m5YJrEjOETL6lF/5g aKYbEko5/Sk5uL6abv8vJCcLZV7igTmP6QuhMO/BeM4PxALX2eB+OS80KTv/EPjQLlXl/E2n KbUvZDAKcQUoa65BABV0oI95BqlEzim19EYkWEGLFJDZh2Hk5DkN0/SLP38F/uygFShnC11y /zYI7HtGJrAI3jbnLfkZ7l96kpcyAQpzdBY4pJZEqoBIO7tVU//rtPYCB44PBKow+fmE9Vyy oMeVnyUD6+WNaPdq16I5uY1L+aQY48VvS7xK/4+6PH2l382hUcdfbW13ZsQcH20A+xqI1+Fb nr0ntcBDWAKsxIiQ+ztkV2OSCJcZ3KvX60n/Tw7E4KnDYLbRo+3mrCB3SG7HodXZm9cEFyMH 23oJM24XKIHbzvXKct8mBQFU6KgQskvz0KArgj/noF7I+Td/GVMro7u2tFz9eDPhwo59TFcA MGU0mXLRGZxyDBbDwQq1bxy9BQugmyI1rJ11qQw/b174vpIVl1/LpvA16lgDNu0XAvdf9CPQ VLgQ9O8ADh3QMhii8QWbRNbHNOvxgvGwzLsG6UcwqeXCZI99LDRw2rqLMZw43nD3aglyVIhR 5gHLnWo05Z27BObHIvViwOcnqeue74b2XvW6GqNxGycsV1KSwVwXI3KWHkeYg3dqtGqrljaQ eqIDrIqehBE1dbEKqZObYjxik5aQf74JNnES2e4mmP1GgzRg73QMczlfGIS2CibA08B++wK1 VCBMwV2RiKoomaESSdrCUqqeUTnt+93tHK8SEYwiQCMdUxokbSvqFYTgrSHRvUf06hh2m9po ihoHFu7w9PdCsaR7wtncqJGZNoh4VBBnWvHvg15N5akIuhsnFkbOwhwukrv0V1wBOAi2YAxs H4kxQxgJL6Ky1hBehuX2JnxPvvcLWyztBGjZqjK203Phc6M8/RqirxwoFHisQe1U0s6pi8/g p8Fjj3GvMyMUFdBNPC5Glw6/BV7ubzANyw05oeOkGZpLbHxqDjJndQgGOoizB+kOdZZKqKNU gHoQKh4T4CjLvInn1+xY1cKJudXoeQvI86ofv2U1bK5J+1gkRqpiG1G5MZ21UfGpE8eAqbYm o0Ixf2VxF7NTCvxgl6noM3ri5tPZTw6EW+2yCyiD4lULP4XH85DGSKlJMu5wc97jpjmVitD9 VKtMFgB3degZRuYa1GVMRR47U0MujTnnCK5y2YxiDQ1tu+F2yeIxe3+dR0BM2oNRW94jF6qL 5Lmx9wdWUGpaUAumn7HrQ7h26VVraJtInXBWkxIcgD5KmhjVu27sb/Kb8NU6ZwuuDlaS6zmO QHcGuO7+UFDlX++V2JFoVJzPymnoJD4gwB3hCqGIXB/oWCYMcB8yBHD5cDNEPtY3z4IXi592 nHcAlmxOcXs/M3Bzc+S9LDjETj7D9sPLHqOr8vIriaw6Gx0DAfqmvmynoeiCg0myWrh0NIsU yzUrRH6a42t1qKgMOshcFM7YT20o8d8BIx6lZM9wZ8K3n1PzI6J8HQOl3X+LcdA0qLzRHUIT D8PhdXS5UK2vS8rZmLM3I//WniHl4F6e9S0a2UE1z4v9MtKBY+b6bVFmW1+pV/y/mezKbBt2 zwaz/Up8nsTheoE7REswiuqCbcXBUBEPCbomkfA/5Wkoa5Qfmrqbamo2R80g4W6FL/b6FI5O j6xatI4ECR39Mk6LF/czCi59NT/YNeJJdML6k/PzlGZ3rATcs5u0KJN33YvOHqh7yN5jbRg1 lo3g8n85M/eegAPtOq4GkIKaGOzPptJvGmr1eEExo6Xx9z9QMsnQGlaGsuwC6rvSmpatOy7Z VnUVmRg7C7KQ/yHWlbPjSUu53PXT8L0azfOfiRflZM6A0DDbE1H3FJNBGV8x8FmUFDsnIu7K Q94/mxDvwGj7EIdlqQwcUG4Czm6xk/gay9oGsLHfVwGs0cbvReTaYvHsapyB30KpMT/6lHdb DXKPUIQSjhYEk2cWwK5Z+fov4KRtbPCQLL5dqqrA/3Gv+VaU73gKYuH9Ixg8n7MM8yOOiMnF Pgnwg9ZWns/Hc3FmjIJQihRliTXbsfdqg3usitw5tuy9vjmQmeNrcOGFqdSPNNz+hu3nbbLN uiegzx8ICpZ0ZVEzGHBybwW1lofwy90cDzlHbMFvC/LBKXe/80fRwYccD92PdBU4rgU2wBMP YvEkIqw2OIlyPEyDFhBWBrqncToLc0GLmehNU/WUUaGMLPVQF+Di8rzYK66VfhRlLAO70z26 WvdSRW6eGjexFyLH1i1POpBjT+WJklbsYC5KFN2DHT7CcjhYVu9OcN2ijs/xfs1gGnLPCgSK 2sZEQsFo7uO4Cdfmvg6FXZG6y8vNvWJlS+f/eTEOI0dsfZDDSF9luYc63M/gegwjmkMVLlul S3eo8Q76UmhifWKwyF7XQBmrz9KgMeUpxwnN/mEsJZHXnnA8VQG6mDaWHFo75N1T9bova5X0 N3Gkqn+fSxD/9zj9swZH8HIKciDPRLJ3jLmHTfVCE0OSjv5bAk3ZmRYmfCWs2KP99009sWql 50JRbtWElcyE6FCYqyANNMHKZZzGDgjlOzD5PM=
- Ironport-sdr: 64f07370_Jtz67SDXhcrsPvvTR7F90bwZVMWJeQ/hJ6hbZ08eB4kU2yX 0x6yOEiHDI8L+fVlBwu9EMtM/j34Z7US/8lN95Q==
----------------------------------------------------------------------------------------------------------
**
** CALL FOR EXTENDED ABSTRACTS
**
** Dafny at POPL 2024
** 1st Workshop on the Dafny Programming and Verification Language
** 14th of January 2024, London, United Kingdom
**
** Submission Deadline:
** October 11, 2023
**
** https://popl24.sigplan.org/home/dafny-2024
** https://dafny24.hotcrp.com/
**
-----------------------------------------------------------------------------------------------------------
* OVERVIEW
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:
- Relation to Hoare logic, Incorrectness logic, Outcome logic, over- and
under-approximation, ...
- Interactive theorem proving and SMT automation
- Coinduction and corecursion
- Dynamic frames vs. separation logic vs. ownership
- Test generation for Dafny
- Specification and proof inference for Dafny
- Extensions and applications of Dafny
- Alternative verifier backends
- Program verification at industry-scale
- Translation to or from Dafny and other languages
- Logical foundations for Dafny (partial functions, nonempty types, extreme
predicates, ...)
- Dafny in teaching
- Comparison with other auto-active program verifiers (SPARK, F*, Why3,
Viper, Whiley, ...)
- Comparison with other proof assistants (Coq, Isabelle/HOL, Lean, ...)
-----------------------------------------------------------------------------------------------------------
** IMPORTANT DATES
-----------------------------------------------------------------------------------------------------------
- Submission: Wednesday, October 11, 2023 (AoE)
- Notification: Wednesday, November 15, 2023
- Workshop: Sunday, January 14, 2024
-----------------------------------------------------------------------------------------------------------
** SUBMISSION GUIDELINES
-----------------------------------------------------------------------------------------------------------
To give a presentation at the workshop, please submit an anonymous extended
abstract (2-6 pages, excluding references) via hotcrp:
Please use the acmart two-column sigplan sub-format LaTeX style to prepare
your submission:
https://www.sigplan.org/Resources/Author/
We don’t intend to publish the workshop’s submissions. However, presentations
may be recorded and the videos may be made publicly available.
-----------------------------------------------------------------------------------------------------------
** CONTACT
-----------------------------------------------------------------------------------------------------------
All questions about submission should be emailed to the program chairs Stefan
Zetzsche (stefanze AT amazon.com) and Joseph Tassarotti (jt4767 AT nyu.edu).
- [Coq-Club] Workshop on Dafny at POPL 24 (Call for Papers), Stefan, 08/31/2023
Archive powered by MHonArc 2.6.19+.