ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic

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

Title
A Behavioural Type System for Mungo with Generics
BEHAPI
A Theory of Contexts for Higher-Order Encodings of Process Algebras
BEHAPI
A Virtual-Machine Metaobject Protocol for Run-Time Software Adaptation
BEHAPI
Adventures in Formalising the Meta-Theory of Session Types
BEHAPI
BehAPI Practices
BEHAPI
BehAPI Year 1 Review and Year 2 projections
BEHAPI
Binary Session Types in Coq
BEHAPI
Formalising session-typed languages without worries
BEHAPI
Hardware Interactions as Behavioural Types.
BEHAPI
Mailbox Types for Unordered Interactions
BEHAPI
Mechanise your proofs in Coq: From zero to cut-admissibility in less than three months.
BEHAPI
Proving properties about Linear Pi in Coq
BEHAPI

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.

You're viewing the program in a time zone which is different from your device's time zone - change time zone

Sat 6 Apr
Times are displayed in 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): Antonio RavaraNOVA University of Lisbon and NOVA LINCS
09:00 - 09:30
Talk
A Theory of Contexts for Higher-Order Encodings of Process Algebras
BEHAPI
Ivan ScagnettoUniversity of Udine
09:30 - 10:00
Talk
Formalising session-typed languages without worries
BEHAPI
Wen KokkeUniversity of Edinburgh
10:00 - 10:30
Talk
Adventures in Formalising the Meta-Theory of Session Types
BEHAPI
Francisco FerreiraImperial College London
11:00 - 12:00: Mechanising Proofs of Behavioural Types for APIsBEHAPI at S4 (BEHAPI)
Chair(s): Luca PadovaniUniversity of Turin
11:00 - 11:20
Talk
Proving properties about Linear Pi in Coq
BEHAPI
Antonio RavaraNOVA University of Lisbon and NOVA LINCS, Marco GiuntiNOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
11:20 - 11:40
Talk
Binary Session Types in Coq
BEHAPI
Ornela DardhaUniversity of Glasgow
11:40 - 12:00
Talk
Mechanise your proofs in Coq: From zero to cut-admissibility in less than three months.
BEHAPI
Marco CarboneIT University of Copenhagen
13:30 - 15:30: Behavioural Types for API-based softwareBEHAPI at S4 (BEHAPI)
Chair(s): emilio tuostoUniversity of Leicester
13:30 - 14:00
Talk
Mailbox Types for Unordered Interactions
BEHAPI
Ugo de'LiguoroUniversità di Torino, Luca PadovaniUniversity of Turin
14:00 - 14:30
Talk
A Behavioural Type System for Mungo with Generics
BEHAPI
A: Hans HüttelDepartment of Computer Science, Aalborg University
14:30 - 15:00
Talk
A Virtual-Machine Metaobject Protocol for Run-Time Software Adaptation
BEHAPI
Guido ChariCzech Technical University, Czechia
15:00 - 15:30
Talk
Hardware Interactions as Behavioural Types.
BEHAPI
Francisco MartinsUniversity of Lisbon
16:00 - 18:00: BehAPI Business MeetingBEHAPI at S4 (BEHAPI)
Chair(s): Adrian FrancalanzaUniversity of Malta
16:00 - 17:00
Talk
BehAPI Practices
BEHAPI
Caroline CaruanaUniversity of Malta
17:00 - 18:00
Meeting
BehAPI Year 1 Review and Year 2 projections
BEHAPI
Adrian FrancalanzaUniversity of Malta