Skip to ContentSkip to Navigation
About us Latest news Events PhD ceremonies

Session-based concurrency: between operational and declarative views

PhD ceremony:Mr M.A. (Mauricio) Cano Grijalba
When:January 07, 2020
Supervisors:J.A. (Jorge) Perez Parra, Prof, prof. dr. G.R. (Gerard) Renardel de Lavalette
Where:Academy building RUG
Faculty:Science and Engineering
Session-based concurrency: between operational and declarative

Communication-based software is ubiquitous nowadays. From e-banking to e-shopping, online activities often involve message exchanges between software components. These interactions are often governed by protocols that explicitly describe the sequences of communication actions that should be executed by each component. Crucially, these protocols are not isolated from a program’s context: external conditions such as timing constraints or exceptional events that occur during execution can affect message exchanges. As an additional difficulty, individual components are typically developed in different programming languages. In this setting, certifying that a program conforms to its intended protocols is challenging.

A widely studied program verification technique uses behavioral type systems, which exploit abstract representations of these protocols to check that the program executes communication actions as intended. Unfortunately, the abstractions offered by behavioral type systems may neglect the influence that external conditions have on the program. This thesis addresses this issue by considering programming languages with declarative features, in which the governing conditions of the program can be adequately described. Our work develops correct translations between programming languages to show that languages with declarative features can indeed articulate a unified view of communication-based programs. Specifically, these translations demonstrate that the operational features of communication-based programs can be correctly represented by languages with declarative features. An additional contribution is a hybrid language that combines the best of both worlds, enabling the analysis of operational and declarative features in communication-based programs.