H2020Individual fellowship2016–2018

PACT · Proof-theoretical Approaches to Concurrency Theory

Horizon 2020 — Marie Skłodowska-Curie Actions

Duration: 2016-10-01 → 2018-09-30
EU contribution: €159,461
Participants: 1
Scheme: MSCA-IF-EF-ST

Lines connect the coordinator with its partners.

Results in brief

Proof-theoretical Approaches to Concurrency Theory

The project was based on the observation that the development of logical foundations had been a very successful methodology in the framework of sequential programming, and proposed to investigate a similar development in the framework of concurrent programming. This is particularly challenging, because the current move from the standard setting towards programs running in a distributed way, potentially on mobile infrastructures, has lead to a very complex theory where safety guarantees are still difficult to obtain. The fundamental question of the project (how to develop well-behaved correspondence between proofs and concurrent programs) also yields important problems in proof theory, where some progress has been made recently in representing proofs in a more parallel ways, but the interaction of sequentiality and parallelism remains obscure. The project was therefore organised in two steps: first, the connection between proofs and programs should be studied in a setting without sequentiality (that is, without the ability to explicitly order actions in a program), and only then should sequentiality be added to expand the expressivity of programs. The main challenge lies in the development of a system offering a representation of proofs flexible enough to capture simple programs in a simple way and yet allow for an extension to arbitrary sequentiality. In order to achieve this, the proof-theoretical investigation has to be guided by the known structure of concurrent programming models: here the guiding perspective was given by the family of languages around the pi-calculus (a mathematical model for concurrent programs), and in particular the solos calculus, in which all actions are parallel cannot be explicity ordered (as a basis for further extension to arbitrary sequentiality).

Data: CORDIS, © European Union

Project objective

This project aims at providing a mathematical understanding of software exploiting modern distributed computer architectures, through the study of type systems for concurrent programs from a logical perspective. Type systems are an essential part of modern programming languages, that have proved to be a reliable support for the development of trustworthy software in the standard setting of sequential (functional) computing. However, the mathematical foundations and associated techniques underlying the type systems of functional programming languages have not yet been transferred to the distributed setting, although this is a crucial step in the development of concurrent programming languages.A cornerstone of the development of functional type systems was the connection between proof systems, in formal logic, and programming languages. Proof theory is a flexible tool that naturally leads to a precise, mathematical specification of type systems that can be very expressive. The goal of the project is to leverage recent work in computational logic (in particular linear logic and its extensions) to design type systems for process calculi (a mathematical representation of distributed software) that support the features necessary to the development of a programming language. Specifically, the question of the sequentiality of computing steps in this parallel setting is the major point of contention, that needs to be addressed for such a programming language to be reasonably conceived. This proof-theoretical approach to concurrency theory (the mathematical study of distributed software) is the key to the development of type systems that would validate well-behaved distributed programs: the main objectives of the project are the integration of explicit sequentiality to state-of-the-art systems, and the establishment of a precise relation between the typeability of a program (its validity according to the type system) and its implementability.

Original text from CORDIS.

Participants

TECHNISCHE UNIVERSITAT BERLIN · BerlinCoordinatorGermany

PACT · Proof-theoretical Approaches to Concurrency Theory

Results in brief

Proof-theoretical Approaches to Concurrency Theory

Project objective

Participants

Links