APIs are software interfaces describing the services, functions or procedures offered by a software component to other components. Behavioural Types are a suite of technologies that elevate flat API descriptions to graph structures describing the intended order of usage. This permits automated analyses for correct API compositions to provide guarantees such as service compliance, deadlock freedom, dynamic adaptation in the presence of failure and load balancing. The BehAPI project aims to bring the existing prototype tools based on these technologies to mainstream programming languages and other API-based technologies.
This workshop will present ongoing research on behavioural types to assist the development of correct protocol-based systems in the large, by members of the project and by other researchers working in the area. The workshop shall be an open event with invited and selected talks. The main aim of the workshop is to foster the dissemination of work, facilitate discussions and enable new potential collaborations. As a result, there will only be a light selection mechanism without formal proceedings.
Accepted Papers
Call for Papers
We solicit the submission of talk abstracts on either theoretical or applied aspects dealing with API-based software construction, including case studies or experience reports. Relevant topics include (but are not limited to):
- Type Systems and Program Logics
- Programming Language Design and Implementation
- Semantic Models of Computation such as process algebra and automata
- Testing, Model Checking and Theorem Proving
- Runtime Monitoring, Verification, Enforcement and Adaptation
Please indicate whether yout talk is a short (15mins), medium (25mins) or long one (45mins). Presentations describing ongoing work-in-progress are also encouraged. Abstract submission will undergo a light reviewing process and involves a firm commitment that one of the authors of the work will attend and participate in the workshop in case the abstract is accepted. There will be no formal proceedings.
Sat 6 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:30 | Mechanising Proofs for Behavioural Types and ProcessesBEHAPI at S4 (BEHAPI) Chair(s): António Ravara NOVA University of Lisbon and NOVA LINCS | ||
09:00 30mTalk | A Theory of Contexts for Higher-Order Encodings of Process Algebras BEHAPI Ivan Scagnetto University of Udine | ||
09:30 30mTalk | Formalising session-typed languages without worries BEHAPI Wen Kokke University of Edinburgh | ||
10:00 30mTalk | Adventures in Formalising the Meta-Theory of Session Types BEHAPI Francisco Ferreira Imperial College London | ||
11:00 - 12:00 | Mechanising Proofs of Behavioural Types for APIsBEHAPI at S4 (BEHAPI) Chair(s): Luca Padovani University of Turin | ||
11:00 20mTalk | Proving properties about Linear Pi in Coq BEHAPI António Ravara NOVA University of Lisbon and NOVA LINCS, Marco Giunti NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa | ||
11:20 20mTalk | Binary Session Types in Coq BEHAPI Ornela Dardha University of Glasgow | ||
11:40 20mTalk | Mechanise your proofs in Coq: From zero to cut-admissibility in less than three months. BEHAPI Marco Carbone IT University of Copenhagen | ||
13:30 - 15:30 | Behavioural Types for API-based softwareBEHAPI at S4 (BEHAPI) Chair(s): emilio tuosto University of Leicester | ||
13:30 30mTalk | Mailbox Types for Unordered Interactions BEHAPI | ||
14:00 30mTalk | A Behavioural Type System for Mungo with Generics BEHAPI | ||
14:30 30mTalk | A Virtual-Machine Metaobject Protocol for Run-Time Software Adaptation BEHAPI Guido Chari Czech Technical University, Czechia | ||
15:00 30mTalk | Hardware Interactions as Behavioural Types. BEHAPI Francisco Martins University of Lisbon | ||
16:00 - 18:00 | |||
16:00 60mTalk | BehAPI Practices BEHAPI Caroline Caruana University of Malta | ||
17:00 60mMeeting | BehAPI Year 1 Review and Year 2 projections BEHAPI Adrian Francalanza University of Malta | ||
| Sat 6 Apr 2019 Workshop |
| Thu 14 Feb 2019 Notifications |
| Thu 31 Jan 2019 Submissions |
