hdr

The defence of my HDR will take place on the 26th March at 15:00 CET in the salle de conference of the Laboratory I3S

The defence will be in English, and will be available online.

Title: Taking a Walk on the Expressiveness Road

Abstract This dissertation explores the intricacies of concurrent systems and their formal analysis, aiming at understanding their behaviors and at verifying their properties through formal methods. Concurrent systems, central to modern computing, involve multiple entities working collectively to shape the system's overall behavior. This research delves into the distinctive challenges posed by these systems. In concurrent systems, the focus shifts from program termination and correctness, typical of sequential systems, to responsiveness at all times. Behaviors become complex, involving interactions, data exchanges, and resource sharing among independent processes or entities. Verification priorities encompass synchronization, communication consistency, and resource management. The dissertation comprises three interconnected research directions: - Process Algebras and Session Types - Communicating Automata - Applications: demonstrating the practical application of formal methods in diverse domains, bioinformatics, ecology and neural network. In summary, this dissertation uncovers the complexities of concurrent systems, emphasizing their formal analysis and aiming to identify the boundary between descriptive power and decidability The dissertation will be organized in chapters discussing my work and classifying them into those three categories: process calculi and session types, automata with memory, applications of concurrent models to various domains. Each chapter will be preceded by a general introduction, specifying and commenting the context and giving pointers to the publications concerning the discussed works.


Jury:

  • Luis Caires, reviewer, professor at Tecnico Lisboa
  • Simon Gay, examiner, professor at the University of Glasgow
  • Paola Giannini, examiner, professor at Università del Piemonte Orientale
  • Etienne Lozes, invited member, professor at Université Côte d’Azur
  • Maciej Koutny, examiner, professor at Newcastle University
  • Roland Meyer, reviewer, professor at University
  • Alan Schmitt, reviewer, DR Inria Rennes Bretagne Atlantique

Manuscript

As a connected event, on the 25/03 and 26/03 there will be a group of seminars. All seminars will be held in the salle de conference of the Laboratory I3S.

25/03 14:00 - 14:45 Kirstin Peters

Mixed Choice in Session Types Session types provide a flexible programming style for structuring interaction, and are used to guarantee a safe and consistent composition of distributed processes. Traditional session types include only one-directional input (external) and output (internal) guarded choices. This prevents the session-processes to explore the full expressive power of the pi-calculus where the mixed choices are proved more expressive than the (non-mixed) guarded choices. The talk is about mixed choice constructs and their expressive power in session types.

Slides

25/03 15:00 - 16:00 Jorge A. Perez

Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks In this talk, I discuss recent work aimed at tackling the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. I shall present two contributions. First, I will present Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. Building upon the Curry-Howard correspondences between linear logic and session types, APCP enjoys essential properties, most notably deadlock-freedom. Second, I will present and illustrate a new concurrent λ-calculus with asynchronous session types, dubbed LAST^n. I will illustrate a precise technical connection between APCP and LAST^n, namely how to soundly transfer the deadlock-freedom guarantee from APCP to LAST^n. The talk will be part of the Forum Numerica series.

Slides

25/03 16:00 Coffee Break

26/03 09:00 Welcome

26/03 09:30 - 10:15 Alan Schmitt

Effects in Skel. From Exceptions to Delimited Computation Skeletal Semantics is a meta-language to describe the semantics of programming languages. We present it through several examples, highlighting how complex features can be captured in a readable way using monads. These features range from simple effects like exceptions to more complex ones like generators.

Slides

26/03 10:30 - 11:15 Paola Giannini

Asynchronous Sessions with Input Races. Joint work with Ilaria Castellani and Mariangiola Dezani. We propose a calculus for asynchronous sessions where input choices with different senders are allowed in processes. We present a type system that accepts such input races provided they do not hinder lock-freedom. To this we define global types in which output and input choices are split. Instead of projection we define typing rules matching directly the global type with the multiparty session and imposing the restrictions needed to enforce input lock-freedom.

Slides

26/03 11:30 - 12:15 Simon Gay

Special Delivery: Programming with Mailbox Types The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the success of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. While many actors may send messages to some actor, only the actor may (selectively) receive from its mailbox. Although actors eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to communication errors such as protocol violations and deadlocks. Mailbox types are a novel behavioural type system for mailboxes first introduced for a process calculus by de Liguoro and Padovani in 2018, which capture the contents of a mailbox as a commutative regular expression. Due to aliasing and nested evaluation contexts, moving from a process calculus to a programming language is challenging. This paper presents Pat, the first programming language design incorporating mailbox types, and describes an algorithmic type system. We make essential use of quasi-linear typing to tame some of the complexity introduced by aliasing. Our algorithmic type system is necessarily co-contextual, achieved through a novel use of backwards bidirectional typing, and we prove it sound and complete with respect to our declarative type system. We implement a prototype type checker, and use it to demonstrate the expressiveness of Pat on a factory automation case study and a series of examples from the Savina actor benchmark suite.