Supervisors

Suitable for

Abstract

Probabilistic session [1] types explores how uncertainty and likelihood influence communication protocols in distributed systems. Extending Probabilistic Resource-Aware Session Types allows for many possibilities, they typing is based on the system of DILL [2] ( a session type system with a Curry Howard isomorphism with linear logic) and can be extended with parallel and restriction similarly alternate rules can be derived from the classical viewpoint [3] expanding typeability. This project is be a mix of both theory and practice where an extension of the implementation NomosPro/PRast. Overall, this extension aims to provide a more comprehensive framework for designing and analysing distributed systems with probabilistic and resource-aware communication protocols. The project also develops bisimulation semantics for concurrent processes.

[1] Probabilistic Resource-Aware Session Types (acm.org) 

[2] concur10.pdf (cmu.edu) 

[3] propositions-as-sessions.pdf (ed.ac.uk)

Pre-requisites: DPTP