Reversibility of the Pi-Calculus and Session Types
Lead Research Organisation:
Imperial College London
Department Name: 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.
Organisations
People |
ORCID iD |
| Nobuko Yoshida (Primary Supervisor) | |
| Eva Graversen (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509486/1 | 01/10/2016 | 31/03/2022 | |||
| 1791132 | Studentship | EP/N509486/1 | 01/10/2016 | 31/03/2020 | Eva 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) |