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] (2nd CfP) Dafny Workshop at POPL 24
- Date: Wed, 27 Sep 2023 15:24:57 +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-wm1-f48.google.com
- Ironport-data: A9a23:YCzMj6wppyPtl1zUN4J6t+dewyrEfRIJ4+MujC+fZmUNrF6WrkUOm zYXDG7UPv7YNDHyfYwlPYu+90hQvZeAy4Q2TAI4qlhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefSAOCU5NfsYkhZXRVjRDoqlSVtkus4hp8AqdWiCmthg /uryyHkEAHjg2Uc3l48sfrZ80s+5quq4lv0g3RnDRx1lA+G/5UqJMlHTU2BByOQapVZGOe8W 9HCwNmRlo8O10pF5nuNy94XQ2VSKlLgFVDmZkl+B8BOtiN/Shkaic7XAhazhXB/0F1ll/gpo DlEWAfZpQ0BZsUgk8xFO/VU/r0X0QSrN9YrLFDm2fF/wXEqfFPRyvduNGYNEbdApM96E14R+ vojMncSO0Xra+KemNpXS8Fpj8UnadbuZcYR5iEmwjbeAvIrB5vERs0m5/cChGZ21p0IRKyOI ZZJAdZsREyojxlnIUsaBps4juq0lGL0czBwp1ecpK5x6G/WpOB0+OG3YICJKoHQG625mG6mn FrJrlTCOS0YG+DG1hC97neNwf/2yHaTtIU6UefQGuRRqFaU3ykYDAAcfUCqpOGwzE+4QdNWb UIOkhfCtoA3/U2vC8b4Bli2/C7CsRkbVN5dVeY97Wlh15bp3upQPUBcJhYpVTDsnJReqeUCh wTRzeD6TydiqqOUQn+7/7KZ52H6cysMIGNIIWdOQQIZ6pOx6Ms+nzDefOZFSaSVt9zSHS2v4 jaoqCNlua4fo/RW3IqG/HfGoQmWmL73ciAP6D/qA12VtjFCWNb9ZqiDy0Tq0vJbHYPIEniDp Cclnuad3sAvDLaMtiqHf8sVFpr05fzfaDz4qnxsFqkH6D6C1SOCf4dRwTcmP2ZvEJ8OVgHIa X/pmzF6xcFsLlrzSoRocaedNt8M8ZHwMfjECtXFcctoYLVqUQ2MoRFVek+b2l7ynHgWka0QP YmRdeCuBy04DZtL4SWXReAP960C3QE7mH3uQK7kwySd0baxYGCfTZEHOgCsasE79Ka1nxXHw e1ANselywRtb8OmW3P5qbUsFFEtKWQ3IbvUqMYNL+6KHVdAKVEbUvTUxessRpxhk6Frjdz3x 3CaWHEJ7HrkhHbCFxeGVWA7VpPrQqREjCwaOQ4CAA+W/kYNMKeVwoURTZ8VRYUc1fdCyKd0R sYVes/bDfVoTC/GygsnbpL8jdJDcRi3tD2KJA6gRiY1RL97Zgnz4tS/VBDexCoPKSuWtMUFv Lyr0D3Ac6cDXwhPCMX3auql6lGM4Vwxvf1UZFSRBPV+Y2Du/5pOBw2rq8QoMuceLRnn7RmL5 Ta8WBs3i7HEnN4ozYPvm6uBkbaML8J/OUh/REzw8re8MHjhzFqJmINvfr6BQmHAaTnS5q6nW ORyysP8Ot0hmHJhkdJ1M5Rv/JIEy+rfnZ1o5SU6IyyTdHWuMK1qHVee18oWtqFt+K5QiTHrZ m2xoOtlKZe7E+K7Nm5JPwc0TPWx5ddNkBno0PkFCkHb5ih2wbm5bXtvLyS80CxzEJYlMacO4 /sQh8oN2gnu1jsoKomniw5XxUStL1sBcbkWiZUBJL/nli8Qk1RkTZPBOHWn/qPVe9FoN280K AS1n4vHvaxXnWDZQkowFF/M/OtTvosPsxZ0120/J0yFt97Gp/0v1jhD2G4TYiUM6TsfyMN1G GxgF3MtFJW05z0y2fRyBTG9KT9OFDiy2xLXyWJQsEb7UkPxdGjGDFNlCNa35EpDrl5tJGlKz oq5llTgfy3hJvzq/y0IXkVglfzvYPpx+iDGm+GlB861JIY7UxW0np6RYXc0lDW/DfMTnEHno cxYzNR0Y4D/Ng8SpPQ1NdDLn/BYAhWJP3dLTvxd7bsEVzOUMi273T+VbVu9YIVRLvjN6lW1E NFqOtkJbRmlySKStXoOMMbg+VOvcCIBv7Luu48HJFLqd5Oapztt9Y3Vr23w2D9tTNJpnsIwb IjWclpu14BWaWR8wwfwQAtsYwJUouXooCXz2em09KMCEJdrXCREbxQpyrXt15mKGFIPwv9X1 T8vo4fZyuVjzcJnmI6E/mCvwemrAYubadlkOzxffziDgR0j/CsOW84oRoHbAjlr
- Ironport-hdrordr: A9a23:Q5Fs86gGY7g34bqMDb5c2b5KiHBQXuEji2hC6mlwRA09TyX4rb HNoB1/73XJYVkqKRcdcLy7Scq9qA3nhPlICPgqTNKftWDd0QPCTL2KhbGC/9SKIVybygcy79 YYT0G8MrHN5JpB4PoSLDPWLz9Z+qj+zElgv4nj80s=
- Ironport-phdr: A9a23:JgeVjR+ZcjKD4P9uWZO2ngc9DxPPW53KNwIYoqAql6hJOvz6uci4Y wqHub401xeJBdydt6gazbKO8ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T 4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglWhjexe69+I Rq5oQnMuMQdnI9uJrosxhfTrXZEZeVbyXl0KV6Pmhr3+9u98oNk/ylMofwq6tROUb/9f6Q2T LxYCCopPmUo78D1thfNUBWC6GIEXmoZjhRHDQ7F7ArnXpjqqSv1qvB92CiBMsLoS70/RCmv4 L1qSB/sjycHKiI5/WTKgcF+kK5XvBSsrAF5zoXJYo+aKeB+c7vdc9wGSmVPQ8VfWSJfDI27d IYAFfYNPeNCoon9u1cDrx2zDhSsCuP1zT9Ig2f707Am0+s/HwHJxgogFM8JvXTPsNX6KqkSX vqzzKjJ0zrDc/JX2Szh54jIbB8suv6MXbdqfsrQzUkjDR/KjlKVqYH8OT6ey+sCvXSB4eV6S eKvl3Aoqxt3ojW3xsohiobHip4Wx13Z+yh13Js5KNO2RkB1f9OqH5ldujyZOodrX88vQ31lt iY+x7AIuZC2fDUHxZY7yhDfaPGKco6F6Q/tWuaWJDd3nnNleLSnihap8EigxfX8Vs2u31ZMt CZFlcPMtn8V2xzT7ciHVudy/l252TqVyw/T7eRELEYpnqTYM54s2qA8moYXvEjZHSL7mF/6g LKIekgn4OSl5Ofqbq3kq5KYLYN4lw7zPrk0lsGwD+k0KBUCU3Sd9O+hzrPs51f5T69PjvAuk qnWrpTaJcMDq668GQBV04Ij5w+xDjejzdgUhHcHIV1GdR6dgIjpPFbOIP/8DfihmVijjDBrx /XeMr3gBJXCMGTDna//cbph70NQ0gk+wNBF655JFL0MI+j/V0DyudDACx82KQ20w+LpCNVn0 YMeXHqCArSFMKzMv1+H/OQvIuiSa48JuTf9MOQq5/7wgnIill8deLOm3ZoTaHyiAvtmJECZb WLqgtgaCWgKpBYxTPT2iF2eVj5ef2u+U7om5j4nEIKmEZvDRoe1jbOd2ye7B4RaaXxCClCRC njlbJ6EWvcJaCKKOMBtiD0EVb67S48gzx6irgH6y6A0ZtbTryYfrNfo0MV/z+zVjxA7szJuX OqH1GTYdH15kGoOD2stwK1xqEpvx0uRyqN4jtRXENVS47VCVQJsZs2U9PBzF92nAlGJRdyOU lvzGr1OYBk0R9M1mZoVZlplXs+lhVbF1jarBLkck/qKAoY1++TSxSu5PN5znlDB0qRplFw6W o1XL2TznbJy+QHVFYPVgV6Sl6uCeqEV3SqL/2CGniKVpE8NaAdrSu3eWGwHIE7frND3/ETHG qSyBLouNBlM1dyZIatHQtLshFRCAvzkPYeWeHq/zkG3AxvA3baQdMzqdmEaiT3aE1QBmhsP8 GyuMAE/AmK+pjubAmA+U13oZEzo/K91r3bTolYc6QaMYgUh0rO0/kRQnvmAU7YJ2blCvi49q jJyFVL73tTMCtPGqRAzNKNbKcgw5ltKzwe7/0R0I4CgIqZ+h1UfbxU/vkXg0A9yA5lBls5ip W0jzQ57I6aVmF1bcDbQ0Zf1M7zRYm78mXLnI7XK11/X1sSb5rUU4/Q1g1rmtQCtUEEl9jQv0 tVY1Wed+oSfFBAbAveTGg488xl3oa2fYzFovduFky0xd/Du4nmei4FMZqNt0BurctZBPbnRE QbzF5dfHM2yMKkwnFPvaBsYPedU/apyPsW8dvLA1rT4WYQo1D+gk2lD55hwl0yW8C8pAPXU0 pgMxeOVwhmcXDfxpFiku8Hz34tDYHtBewj3gTihH4NXaqBoKMwQFWqgKsuly8lsnJXtVlZX8 VeiAxUN38rjKn/wJxTtmAZX00oQu3munyC1mid1nz8epa2axCXSwu7meXLrI0ZzTXJ5xRfpK Imw1ZUBWVSwKhIun12j7Fr7wK5SoOJ+KXPSSAFGZXq+I2ZnW6q2/r2MBqwHoIg0vCteVvaxf UKBQb7wixQf2iLnWWBZwXg3eiqrtZPwgxFhwDjFfTAj8TyAI5E2mUeX7ce5J7YZxjccQShkl TTbTkOxOdWk55TclpvOtPy/S3P0U5RSdSfxyobT/CC/5GBsHVi+h6XpwoyhQVV8iHWrkYU6B kCq5F7mb4Lm1rq3K7did0hsXhrn7tZiX5t5mc02jY0R3n4TgtOU+2AGmCH9K4Y+u+q2YXwTS DoM29OQ7hLi3RgpNW6EyYv/RHiB0NBqZ9SSbWYf2yZ75MdPQvTxjvQMjW5ur1y0oBiEK+Nhk zkUz+kj9GwBiOEEkAUoxySZRLsVGAMLWE6k3wTN5Ne4oqJNYW+perXlz0tyk+eqC7Saqx1dU nL0Kd8yWDV95cJlPBfQwWX+v8v6LcLIY4tZ5Xj221/QyvJYI5Urmr8WiDp7bCjj6GY9xbdzj AQyj8rn+tHWcyM3oP3/WlkCanX0f59BpG2r1/0F2J/Ih8b3Wcwwf1dDFJrwEaD2TnRL7a6hb 0DWV2dk4naDReiBQ0nFtBYg/yqJS9fxbzmWPCVLko8kHUXbfR0FxlhTBWVf/NZxFxj2lpO9N h4ju3ZJoAa/80UEy/o0ZUCnAiGG+1juOnFsD8LGZBtOslMbuByTaJ3CqLo1R2YBoPjD5ESMM jDJPVwZSzFUHBXeVxa7eeDxrdjYr7rCX7T4cquIOOTU77QZDqbAxIrzgNE/oXDWbZTJZSMkV 7piiy8hFThvEsDd0V3jUgQxkCTAJ46erRa4oGhsq9ynte7sU0Tp7JeODL1bNZNu/Qq3iOGNL bzYgiExMjte2p4WoB2AgLECwF4fjT1vfDixAPwBsyDKVqfZhq5QCVYSdSpyMMJC66900BNKP IbXjdb817gwifBQaR8NTVv6hsSgftAHOUm4PVLDQVmObfGIeW2NzMbwbqexD7ZXiaQcthG9v yqaD162PjmHkGqMNVjnOuVNgSeHeR1G7dvlI1A9VC66FoKgNk3oVb0/xSc7yrA1mH7QYGsVM DwmNlhIsqXV9yRTxPN2B21G6HNha+iCgSeQqefCefN0+bNmBDp5k+VC7TE00bxQuWtfWPF7k S3Ao8J8uFqmn8GAzzNmVFxFrTMB1+fp9Q1yfL7U8JVNQyOO5BUW8WCZEAgHvfNgA9zr/r9Vk 53ByPK1JzBF/NbZu8AbAoKHTaDPeGpkOh3vFjnOCQIDRjP+LmDTiXtWl/SK/2GUpJw3wnANs J8HS7seS1lsU/1GWgJqG9sNJJoxVTQhw+bzZCsg6n+3rR2XT8Jf7Mivvh26DvDmKTLfhr5BN UJg/A==
- Ironport-sdr: 65143b4d_0qZMKECoRyqWjpWcQUSqK1gb5PQm4reqSMsVoPlBg47DufK eVpjlQxNehCNUobUe5DP9pewz4UR58B142ntvqA==
----------------------------------------------------------------------------------------------------------
**
** Update: Program Committee
**
----------------------------------------------------------------------------------------------------------
**
** 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
-----------------------------------------------------------------------------------------------------------
** ORGANISATION
-----------------------------------------------------------------------------------------------------------
Program Chairs:
- Joseph Tassarotti (New York University)
- Stefan Zetzsche (Amazon Web Services)
Program Committee:
- Adam Chlipala (Massachusetts Institute of Technology)
- Jean-Christophe Filliatre (CNRS)
- Andrea Lattuada (VMware Research Group)
- Elaine Li (New York University)
- Peter Müller (ETH Zurich)
- Nadia Polikarpova (University of California, San Diego)
Steering Committee:
- Rustan Leino (Amazon Web Services)
- Jean-Baptiste Tristan (Amazon Web Services)
-----------------------------------------------------------------------------------------------------------
** 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] (2nd CfP) Dafny Workshop at POPL 24, Stefan, 09/27/2023
Archive powered by MHonArc 2.6.19+.