VEST'21
Online on 12 July 2021
2nd workshop on verification of session types
Co-Located with ICALP'21
The goal of this workshop is to bring together Researchers and build 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 behavioral types (in the US and Europe) 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 became 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, mechanically 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 weak liveness property, mechanical 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.
Invited Speakers
Jesper Bengtson
IT University of Copenhagen, Denmark
Andreia Mordido
University of Lisbon, Portugal
The Mobility Group
Tutorial jointly delivered by:
David Castro-Perez (University of Kent, UK)
Francisco Ferreira-Ruiz (Imperial College London, UK)
Lorenzo Gheri (Imperial College London, UK)
Call for talks
Type of contributions:
We request two kinds of research contributions:
Short presentations (1 page) of work published elsewhere;
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:
Regular Talks Submission: Monday,
3rd May 202124th May 2021Regular Talks Notification: Monday,
14th June 202121st June 2021Final Version: Monday, 5th July 2021
Short Talks Submission: Monday, 21st June 2021
Short Talks Notification: Friday, 25th June 2021
Workshop: Monday, 12th July 2021
Submission Link
Programme 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
For enquires, please contact the PC Co-Chairs: O. Dardha or A. Ravara.