Reversibility of the Pi-Calculus and Session Types

Lead Research Organisation: Imperial College London
Department Name: Dept of Computing

Abstract

This project studies reversible computation of the pi-calculus based on session types and multiparty session types. It includes behavioural theories and their applications.

Publications

10 25 50
publication icon
Graversen E (2017) Towards a Categorical Representation of Reversible Event Structures in Electronic Proceedings in Theoretical Computer Science

publication icon
Graversen E (2019) Towards a categorical representation of reversible event structures in Journal of Logical and Algebraic Methods in Programming

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509486/1 01/10/2016 30/09/2021
1791132 Studentship EP/N509486/1 01/10/2016 31/03/2020 Eva Fajstrup Graversen
 
Description Event structure semantics of 3 different reversible process calculi (CCSK, PiIK, and PiIH) have been defined, which has provided a better model of the dependencies between actions in the process calculi. Comparing the event structure semantics of PiIK and PiIH has proved an equivalence between the two calculi.

A common operator for controlling reversibility, rollback, has been added to CCSK and modelled by event structures.

Dual semantics of rollback and commit have been described and used to simplify implementing certain protocols.
Exploitation Route We has begun work on how rollback and commit might be implemented and used to simplify implementation of distributed protocols and transactions. This could be used to implement any number of protocols.

We have used reversible event structures to clarify the causal relationships in concurrent reversible programs, something that is very important for reversible semantics.
Sectors Digital/Communication/Information Technologies (including Software)