Last Saturday, the BehAPI workshop at ETAPS successfully took place, where speakers both from within and outside the project gave a number of interesting talks about Mechanising Proofs for Behavioural Types and Processes, and Behavioural Types for API-based software. In the final part of the workshop, an internal meeting was conducted, where project matters such as secondments and the upcoming Leicester summer school were discussed.
Attendees from within the project included Adrian Francalanza (UOM), Emilio Tuosto (ULEIC), Antonio Ravara (NOVA), Hernan Melgratti (UBA), Laura Bocchi (UKENT), Ornela Dardha (UGLA), Roland Kuhn (ACT), Stephanie Balzers (CMU), Hans Huttel (AAU), Marco Carbone (ITU), Luca Padovani (UNITO) and Mario Bravetti (UNIBO).
The following presentations were given
- Ivan Scagnetto – A Theory of Contexts for Higher-Order Encodings
- Wen Kokke – Formalising Session-Typed Languages Without Worries
- Franciso Ferreira – Adventures in Formalising the Meta-Theory of Session Types
- Antonio Ravara – π without α – a certified implementation
- Ornela Dardha – Session Types in Coq
- Marco Carbone – Mechanising Your Proofs in Coq
- Ugo de’Liguoro and Luca Padovani – Mailbox Types for Unordered Interactions
- Hans Huttel – A behavioural type system for Mungo with generic classes
- Guido Chari – A Virtual-Machine Metaobject Protocol for Runtime Software Adaptation
