<
Laura Voinea

Laura Voinea

Research Associate @ University of Kent

Laura is a Research Associate at the University of Kent, working on the EPSRC project 'Session Types for Reliable Distributed Systems (STARDUST)'.

She is interested in using type systems for communication protocols, known as behavioural types, for statically and dynamically verifying communication programs. Her current research focus is on reliability and time properties for distributed actor systems.

Past Activities

Laura Bocchi / Laura Voinea
Code BEAM V Europe
20 May 2021
13.10 - 13.50

Compositional protocol engineering for communicating actors

In systems of communicating processes or actors, data types can be used to discipline the sorts of sent and received messages. Session types, in addition, can describe specific causalities and patterns among different send/receive actions (like application-level protocols). I will give an overview on recent and ongoing research about writing “good protocols” using session types and session types to yield correct implementations.    

I will then focus on modular composition of protocols.  Real-world communication protocols are often built out of simpler protocols that cater for some specific functionality (e.g., banking, authentication) or operate at different levels of abstraction (e.g., HTTP, POP). However much of the work used for program verification (e.g., session types) treat protocols as monolithic units.  

I will show an approach to protocol composition, including a tool that extracts models from concurrent Erlang code into a protocol language based on session types, implements an algorithmic notion of protocol composition, and provides code generation from protocols. The purpose is greater modularisation and code reuse.