[TYPES/announce] Post-doc position at University of Glasgow, UK (PL theory, behavioural types)

[Simon Gay]

University of Glasgow
College of Science and Engineering
School of Computing Science

Research Assistant / Associate
Ref: 037408
Grade 6/7: £32,332 - £36,024 / £39,347 - £44,263 per annum

We have a position for a research assistant / associate in the
theory, design and implementation of programming languages. This
position is associated with the EPSRC-funded project "STARDUST: Session 
Types for Reliable Distributed Systems" (https://urldefense.com/v3/__https://epsrc-stardust.github.io/__;!!IBzWLUs!QjRFFiqaFuzZn7F8rXiErjIM2p_9xY6CwCMI-43nKESM0La6PtiMGVvBS9JslhIeRKrVKoAwpbYwCmyzeCVa7RHWj1-yJrMSO9Dr4jc$ ).

The position is available from 1st June 2024 (or a date to be agreed) to 
31st July 2026.

The position is based in Glasgow, and working in the office at least 
three days per week is expected.


*Project Description*

Distributed software systems are an essential part of the infrastructure 
of modern society. Such systems typically comprise diverse software 
components deployed across networks of hosts. Ensuring their reliability 
is challenging, as software components must correctly communicate and 
synchronise with each other, and any of the hardware or software 
components may fail. Failure and service "outage" is extremely costly, 
with worldwide financial losses due to software failures in 2017 
estimated at US$1.7tn, up from US$1.1tn in 2016.

Failures can occur at all levels of the system stack: hardware, 
operating systems, networks, software, and users. Here we focus on using 
advanced programming language technologies to enable the software level 
to handle failures that arise from any level of the stack. Our aim is to 
provide software-level reliability for distributed systems by combining 
fault prevention with fault tolerance. The key objective is to combine 
the communication-structuring mechanism of session types with the 
scalability and fault-tolerance of actor-based software architectures.

The result will be a well-founded theory of reliable actor programming, 
supported by a collection of libraries and tools, and validated on a 
range of case studies. Key aims are to deliver tools that provide 
lightweight support for developers – e.g. warning of potential issues – 
and to allow developers to continue to use established idioms. By doing 
so we aim to deliver a step change in the engineering of reliable 
distributed software systems.

The project is a collaboration between the University of Glasgow 
(Professor Simon Gay, Professor Phil Trinder and Dr Simon Fowler), the 
University of Oxford (Professor Nobuko Yoshida) and the University of 
Kent (Professor Simon Thompson and Dr Laura Bocchi). The industrial 
partners are Actyx AG, Erlang Solutions Ltd, Quviq AB and Tata 
Consultancy Services.


*Principal Duties*

The main achievement so far of the Glasgow part of the STARDUST project 
is the development of mailbox typing for a core actor language, 
published at ICFP 2023 (https://urldefense.com/v3/__https://simonjf.com/writing/pat.pdf__;!!IBzWLUs!QjRFFiqaFuzZn7F8rXiErjIM2p_9xY6CwCMI-43nKESM0La6PtiMGVvBS9JslhIeRKrVKoAwpbYwCmyzeCVa7RHWj1-yJrMSiYaF2Ek$ ). Mailbox 
types characterise the unordered contents of mailboxes and allow static 
detection of a range of errors related to the production and consumption 
of messages. The successful candidate will be responsble for further 
theoretical work on mailbox typing, in parallel with and in support of 
ongoing work on the design and implementation of a mailbox typing tool 
for Erlang/Elixir.

You should have, or be close to completion of, a PhD in a relevant area, 
or have comparable experience; an awarded PhD or equivalent experience 
is necessary for appointment at Grade 7. You should have a track record 
of publication and communication of research results, strong programming 
and software engineering skills, and a strong background in programming 
languages, including type systems and implementation. It is desirable 
also to have one or more of the following: a combination of theoretical 
and practical skills; knowledge of the theory or practice of concurrent 
and distributed systems; knowledge of the theory or practice of 
actor-based languages;
knowledge of the theory of behavioural types.

We seek applicants at an international level of excellence. The School 
of Computing Science at the University of Glasgow has an international 
research reputation, and Glasgow, Scotland's largest city, offers an 
outstanding range of cultural resources and a high quality of life. The 
successful applicant will be part of the FATA Section and the 
Programming Languages Theme. FATA is a large, friendly, and active 
research group in theoretical computer science, including algorithms and 
complexity, programming language foundations and formal methods. The 
Programming Languages Theme comprises researchers interested in 
programming languages from theory, systems, and education. We have a 
regular seminar series, PLUG, and members of the theme regularly publish 
in top venues (e.g., POPL, ICFP, ECOOP, ESOP, CONCUR). We are also 
members of the Scottish Programming Languages Institute and participate 
in activities such as the Scottish Programming Languages Seminar and the 
Scottish Programming Languages and Verification Summer School.

It is the University of Glasgow’s mission to foster an inclusive 
climate, which ensures equality in our working, learning, research and 
teaching environment.

We strongly endorse the principles of Athena SWAN, including a 
supportive and flexible working environment, with commitment from all 
levels of the organisation in promoting gender equity.



*Further information*

For informal enquiries or further information about the project,
please contact Professor Simon Gay <Simon.Gay at glasgow.ac.uk>,
Professor Phil Trinder <Phil.Trinder at glasgow.ac.uk> or Dr Simon Fowler 
<Simon.Fowler at glasgow.ac.uk>.

*Application details*

Online advert at jobs.ac.uk:

https://urldefense.com/v3/__https://www.jobs.ac.uk/job/DFG143/research-assistant-associate__;!!IBzWLUs!QjRFFiqaFuzZn7F8rXiErjIM2p_9xY6CwCMI-43nKESM0La6PtiMGVvBS9JslhIeRKrVKoAwpbYwCmyzeCVa7RHWj1-yJrMSga4nEg0$ 

Glasgow University online application system:

https://urldefense.com/v3/__https://www.gla.ac.uk/it/iframe/jobs/__;!!IBzWLUs!QjRFFiqaFuzZn7F8rXiErjIM2p_9xY6CwCMI-43nKESM0La6PtiMGVvBS9JslhIeRKrVKoAwpbYwCmyzeCVa7RHWj1-yJrMSbtqN6Js$  (enter reference 136868)

Closing date: 29th February 2024


The University of Glasgow, charity number SC004401.