[TYPES/announce] Fully Funded PhD Position in Refactoring Fault-Tolerant Session Types

[Adam Barwell]

Dear all,

We have a fully funded PhD scholarship available in the School of Computer Science at the University of St Andrews on ‘Refactoring Fault-Tolerant Communication Protocols’.

Any potential candidates are advised to contact Adam Barwell (adb23 at st-andrews.ac.uk) for more information. Formal applications can be made through the School’s postgraduate research portal [1].

A description of the project can be found below and full details of the project can be found here: https://urldefense.com/v3/__https://www.findaphd.com/phds/project/refactoring-fault-tolerant-communication-protocols/?p165748__;!!IBzWLUs!Vmjnp7wt0f_QN37wtPKm3z2zlPfU99UK_N5vO_8KAND5DFYHTsqT4fyYifuNrkYM1w-imOp0D5TxdB-IfDE53oi8RzbwbJQYKP4$ 

The positions are open for both UK and international applications.

Kind regards,

Adam

[1] https://urldefense.com/v3/__https://www.st-andrews.ac.uk/computer-science/prospective/pgr/how-to-apply/__;!!IBzWLUs!Vmjnp7wt0f_QN37wtPKm3z2zlPfU99UK_N5vO_8KAND5DFYHTsqT4fyYifuNrkYM1w-imOp0D5TxdB-IfDE53oi8RzbwRSHDJuU$ 

----

Project Title: Refactoring Fault-Tolerant Communication Protocol

Concurrent and distributed systems are now standard. Yet programming approaches have failed to keep pace. These systems are prone to a range of subtle and difficult-to-debug errors, e.g. communication mismatches, deadlocks, and livelocks. Session Types aim to address these issues via high-level formal specifications of communications protocols. An advantage of this approach is that session types enable static guarantees of desirable behavioural properties, e.g. deadlock-freedom and liveness.

Recent work has focussed on extending session types to support fault-tolerance, enabling protocols with real-world crash-handling behaviours, e.g. failover and the circuit-breaker pattern. Furthermore such approaches enable a gradual approach to introducing failure-handling, whereby a fully reliable protocol can be made fault-tolerant one participant at a time. Nevertheless, a fault-tolerant protocol can be significantly larger and more complex than the fully-reliable protocol from which it is derived. Moreover, ensuring that the desired transformations are effected uniformly and correctly both from a protocol and implementation perspectives can be a laborious and error-prone process.

This PhD project will address this issue by leveraging semi-automatic program transformation techniques from refactoring to develop automatic methods to introduce and manipulate fault-tolerant behaviours in communications protocols. The project will explore the theoretical underpinnings of such transformations, ensuring that the guarantees provided by session types are preserved. Additionally, the project aims to develop tooling to enable application of the developed techniques to real-world code.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20231127/8720e798/attachment-0001.htm>