Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: community: events

Topic: Dafny Workshop at POPL 24

Stefan Zetzsche (Aug 30 2023 at 12:37):

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

https://dafny24.hotcrp.com

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@amazon.com) and Joseph Tassarotti (jt4767@nyu.edu).