[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
*********************************************************************
VEST 2021: 2nd Workshop on Verification of Session Types
Online on July 12, 2021, co-located with ICALP 2021
https://sites.google.com/view/vest21/home
<https://sites.google.com/view/vest21/home>
Submission: Monday, 3rd May 2021
Call for Talks
*********************************************************************
* Presentation
The goal of this workshop is to bring together researchers and build and
strengthen a community working on verification of session types using various
theorem provers such as Agda, Coq, Isabelle or any other.
Session types are abstract representations of the sequences of operations that
computational entities (such as channels or objects) must perform. Stateful
entities offer services in a non-uniform way (one cannot pop from an empty
stack); traditional type systems cannot guarantee that operations are only
invoked when the entity is in the right state.
Large-scale software systems rely on message-passing protocols: their
correctness largely depends on sound protocol implementations. Session types
can help in the specification of correct-by-construction systems, and in
verifying that programs respect their intended protocols.
Recent years have seen a steady stream of research on behavioural types: their
foundations and their transfer to several programming languages. This has led
to highly-cited papers in conferences such as POPL and journals such as TOPLAS.
Research projects on behavioural types have advanced the theory and
applications of behavioural types.
Although the foundations of session types are now well established, and new
works build on approaches that have become standard, there is still a lack of
reusable libraries, namely machine-verified ones. As on one hand the basis of
most works is common, and on the other hand the complexity of the formal
systems is considerable and may lead to errors in the proofs of the soundness
results, machine verifying the type systems proposed is vital. Libraries, or at
least clear formalisations of common approaches, is crucial to avoid not only
to repeat work but also to increase the confidence in the knowledge base.
Moreover, as many of these systems have a goal to do static analysis to ensure
some safety or liveness property, machine verification of these approaches
leads to certified software for program analysis.
The goal of the VEST workshop is to gather the researchers working on
mechanisations of behavioural types using various theorem provers, such as
Agda, Coq, Isabelle or any other. The workshop will be a platform to present
both the now well-established efforts and the ongoing works the community has
put on verification. The workshop will also be a forum to discuss strengths and
weaknesses of existing approaches, potential obstacles and to foster
collaboration.
* Types of Contributions
We request two types of research contributions.
Type 1: Short presentations (1 page) of work published elsewhere;
Type 2: Presentations (2-5 pages) of ongoing original work.
Submissions of Type 1 will consist of 1 page papers presenting the work, the
publication venue and the significance of the results; the PC will select the
submissions with a ranking system.
Submissions of Type 2 will consist of 2 - 5 page papers submitted to a light
reviewing process.
There will be no proceedings of VEST'21, but rather the aim is to strengthen
and further expand our community.
* Important Dates AoE (UTC-12h)
Submission: Monday, 3rd May 2021
Notification: Monday, 14th June 2021
Final Version: Monday, 5th July 2021
Workshop: Monday, 12th July 2021
* Submission Link:
https://easychair.org/conferences/?conf=
<https://easychair.org/conferences/?conf=beat2019>vest21
* Invited Speakers:
- Jesper Bengtson (IT University of Copenhagen, Denmark)
- Andreia Mordido (University of Lisbon, Portugal)
*Tutorial, jointly delivered by:
- David Castro-Perez (University of Kent, UK)
- Francisco Ferreira-Ruiz (Imperial College, UK)
- Lorenzo Gheri (Imperial College, UK)
* Program Committee:
- Robert Atkey, University of Strathclyde, UK
- Laura Bocchi, University of Kent, UK
- Ornela Dardha, University of Glasgow, UK (Co-chair)
- Cinzia Di Giusto, Université Côte d'Azur, CNRS, I3S, France
- Wen Kokke, The University of Edinburgh, UK
- Robbert Krebbers, Radboud University Nijmegen, Netherlands
- Luca Padovani , Università di Torino, Italy
- Kirstin Peters, TU Darmstadt, Germany
- António Ravara, NOVA University of Lisbon, Portugal (Co-chair)
- Ivan Scagnetto, University of Udine, Italy
- Peter Thiemann, Universität Freiburg, Germany
