<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><span id="docs-internal-guid-c5ed194b-7fff-9238-0a76-4ea16302e1e5" class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><font color="#000000" face="Arial" class=""><span style="caret-color: rgb(0, 0, 0); font-size: 14.666666984558105px; white-space: pre-wrap;" class="">*********************************************************************</span></font></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="color: rgb(0, 0, 0); font-family: Arial; font-size: 11pt; white-space: pre-wrap;" class="">VEST 2021: 2nd Workshop on Verification of Session Types</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="color: rgb(0, 0, 0); font-family: Arial; font-size: 11pt; white-space: pre-wrap;" class=""><br class=""></span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class=""><b class="">Online </b>on<b class=""> July 12, 2021</b>, co-located with ICALP 2021</span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><a href="https://sites.google.com/view/vest21/home" style="text-decoration:none;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(17, 85, 204); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; text-decoration: underline; text-decoration-skip: none; vertical-align: baseline; white-space: pre-wrap;" class="">https://sites.google.com/view/vest21/home</span></a></div><div class=""><span class=""><br class=""></span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class=""><b class="">Submission: Monday, 3rd May 2021</b></span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class=""><b class=""><br class=""></b></span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class=""><div style="caret-color: rgb(255, 255, 255); color: rgb(255, 255, 255); font-family: Helvetica; font-size: 14px; white-space: normal; line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">Call for Talks</span></div></span></div><div class=""><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><font color="#000000" face="Arial" class=""><span style="caret-color: rgb(255, 255, 255); font-size: 14.666666984558105px; white-space: pre-wrap;" class="">*********************************************************************</span></font></div></div><div class=""><font color="#000000" face="Arial" class=""><span style="caret-color: rgb(255, 255, 255); font-size: 14.666666984558105px; white-space: pre-wrap;" class=""><br class=""></span></font></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="color: rgb(0, 0, 0); font-family: Arial; font-size: 11pt; white-space: pre-wrap;" class="">* Presentation</span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">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.</span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">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.</span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">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.</span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">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.</span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">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.</span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">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.</span></div><br class=""><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">* Types of Contributions</span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">We request two types of research contributions.</span></div><ul style="margin-top:0;margin-bottom:0;padding-inline-start:48px;" class=""><li dir="ltr" style="list-style-type: disc; font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre;" aria-level="1" class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><b class=""><span style="font-size: 11pt; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">Type 1:</span><span style="font-size: 11pt; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class=""> Short presentations</span><span style="font-size: 11pt; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class=""> (1 page) of work published elsewhere;</span></b></div></li><li dir="ltr" style="list-style-type: disc; font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre;" aria-level="1" class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><b class=""><span style="font-size: 11pt; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">Type 2: Presentations</span><span style="font-size: 11pt; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class=""> (2-5 pages) of ongoing original work.</span></b></div></li></ul><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">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.</span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">Submissions of Type 2 will consist of 2 - 5 page papers submitted to a light reviewing process.</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><br class=""></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">There will be <b class="">no proceedings</b> of VEST'21, but rather the aim is to strengthen and further expand our community.</span></div><br class=""><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">* Important Dates AoE (UTC-12h)</span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class=""><b class="">Submission: Monday, 3rd May 2021</b></span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">Notification: Monday, 14th June 2021</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">Final Version: Monday, 5th July 2021</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">Workshop: Monday, 12th July 2021</span></div><br class=""><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">* Submission Link:</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><a href="https://easychair.org/conferences/?conf=beat2019" style="text-decoration:none;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(17, 85, 204); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; text-decoration: underline; text-decoration-skip: none; vertical-align: baseline; white-space: pre-wrap;" class="">https://easychair.org/conferences/?conf=</span></a><span style="font-size: 11pt; font-family: Arial; color: rgb(17, 85, 204); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; text-decoration: underline; text-decoration-skip: none; vertical-align: baseline; white-space: pre-wrap;" class="">vest21</span></div><br class=""><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">* Invited Speakers:</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Jesper Bengtson (IT University of Copenhagen, Denmark)</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Andreia Mordido (University of Lisbon, Portugal)</span></div><div class=""><span class=""><br class=""></span></div><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">*Tutorial, jointly delivered by:</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- David Castro-Perez (University of Kent, UK)</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Francisco Ferreira-Ruiz (Imperial College, UK)</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Lorenzo Gheri (Imperial College, UK)</span></div><br class=""><br class=""><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">* Program Committee:</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Robert Atkey, University of Strathclyde, UK</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Laura Bocchi, University of Kent, UK</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Ornela Dardha, University of Glasgow, UK (Co-chair)</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Cinzia Di Giusto, Université Côte d'Azur, CNRS, I3S, France</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Wen Kokke, The University of Edinburgh, UK</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Robbert Krebbers, Radboud University Nijmegen, Netherlands</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Luca Padovani , Università di Torino, Italy</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Kirstin Peters, TU Darmstadt, Germany</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class=""><div style="caret-color: rgb(255, 255, 255); color: rgb(255, 255, 255); font-family: Helvetica; font-size: 14px; white-space: normal; line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- António Ravara, NOVA University of Lisbon, Portugal (Co-chair)</span></div></span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Ivan Scagnetto, University of Udine, Italy</span></div><div style="line-height: 1.38; margin-top: 0pt; margin-bottom: 0pt;" class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class="">- Peter Thiemann, Universität Freiburg, Germany</span></div><div class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class=""><br class=""></span></div><div class=""><span style="font-size: 11pt; font-family: Arial; color: rgb(0, 0, 0); font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; vertical-align: baseline; white-space: pre-wrap;" class=""><br class=""></span></div></span></body></html>