[TYPES/announce] (Extended Deadline) Dafny Workshop at POPL 24

[Stefan]

----------------------------------------------------------------------------------------------------------
**
**    Update: Extended Deadline
**
----------------------------------------------------------------------------------------------------------
**
**    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 18, 2023
**
**    https://urldefense.com/v3/__https://popl24.sigplan.org/home/dafny-2024__;!!IBzWLUs!S-gSuH3NQU2QznUp_Jeoxu5kNz5g8YNUhbPKmZ-h2qYF-1gigzoFGvRai2cK4UvhCUrAMhkYSn6n2KnNmm1Gq_8bxoIPmz-I801kb0U$ 
**    https://urldefense.com/v3/__https://dafny24.hotcrp.com/__;!!IBzWLUs!S-gSuH3NQU2QznUp_Jeoxu5kNz5g8YNUhbPKmZ-h2qYF-1gigzoFGvRai2cK4UvhCUrAMhkYSn6n2KnNmm1Gq_8bxoIPmz-I_skQc7A$ 
**
-----------------------------------------------------------------------------------------------------------

* 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 18, 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:

https://urldefense.com/v3/__https://dafny24.hotcrp.com__;!!IBzWLUs!S-gSuH3NQU2QznUp_Jeoxu5kNz5g8YNUhbPKmZ-h2qYF-1gigzoFGvRai2cK4UvhCUrAMhkYSn6n2KnNmm1Gq_8bxoIPmz-I8nEiA9A$  <https://urldefense.com/v3/__https://dafny24.hotcrp.com/__;!!IBzWLUs!S-gSuH3NQU2QznUp_Jeoxu5kNz5g8YNUhbPKmZ-h2qYF-1gigzoFGvRai2cK4UvhCUrAMhkYSn6n2KnNmm1Gq_8bxoIPmz-I_skQc7A$ >

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

https://urldefense.com/v3/__https://www.sigplan.org/Resources/Author/__;!!IBzWLUs!S-gSuH3NQU2QznUp_Jeoxu5kNz5g8YNUhbPKmZ-h2qYF-1gigzoFGvRai2cK4UvhCUrAMhkYSn6n2KnNmm1Gq_8bxoIPmz-IKmst2YY$ 

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 <mailto:stefanze at amazon.com>) and Joseph Tassarotti (jt4767 at nyu.edu <mailto:jt4767 at nyu.edu>).

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20231016/cc642c6b/attachment-0001.htm>