[TYPES/announce] A PhD position at Imperial College London

[Yoshida, Nobuko]

The starting date: 1st October 2019 (3.5 Years)
The position is fully funded, covering tuition fees and a bursary.
The position is available to home and EU students.

The Department of Computing at Imperial College London is a leading
department of Computer Science among UK Universities, and has
consistently been awarded the highest research and teaching (rated as
"Excellent" in the previous national assessment of teaching quality).

We invite applications for a PhD studentship funded by VeTSS in
programming languages and software engineering research related to
concurrency theories and session types under the supervision of
Professor Nobuko Yoshida and Dr Rumyana Neykova.

The primary objective of the PhD project is verification of
distributed protocols using session types.

Session types (also called protocols) are a typing discipline to
structure and verify message-passing communications. Session types (or
behavioural types) have been applied to concurrent/distributed main
stream languages, including Scala [PLDI'19<http://mrg.doc.ic.ac.uk/publications/verifying-message-passing-programs-with-dependent-behavioural-types/>], Go
[POPL'19<http://mrg.doc.ic.ac.uk/publications/distributed-programming-using-role-parametric-session-types-in-go/>,ICSE'18<http://mrg.doc.ic.ac.uk/publications/a-static-verification-framework-for-message-passing-in-go-using-behavioural-types/>,POP'17<http://mrg.doc.ic.ac.uk/publications/fencing-off-go-liveness-and-safety-for-channel-based-programming/>] and F# [CC'18<http://mrg.doc.ic.ac.uk/publications/a-session-type-provider/>].

Session types are also well-connected to several foundational areas
such as automata theories/model-checking [CAV'19<http://mrg.doc.ic.ac.uk/publications/verifying-asynchronous-interactions-via-communicating-session-automata/>,POPL19b<http://mrg.doc.ic.ac.uk/publications/less-is-more-multiparty-session-types-revisited/>] and
Game Semantics/Linear Logic [POPL19c<http://mrg.doc.ic.ac.uk/publications/two-sides-of-the-same-coin-session-types-and-game-semantics/>,FoSSaCs'19<http://mrg.doc.ic.ac.uk/publications/causality-in-linear-logic/>].

See http://mrg.doc.ic.ac.uk/ for more details
on session types and applications.

This research will centre on the hypothesis that: (1) multiparty
session types, and their development approach, can be effectively
extended to deal with data and control-flow constraints; and (2) the
effectiveness of the approach (in a mainstream language) can be
demonstrated via a concrete embedding of the theory. A successful
candidate will develop the underlying theory and language
implementation.

The PhD candidate will be part of the Mobility and Session Types
Research Group (MRG). Informal inquiries about this position are also
encouraged and can be directed to Nobuko Yoshida.

Applicants are expected to have a First Class or Distinction Masters
level degree, or equivalent, in a relevant scientific or technical
discipline, such as computer science. Applicants must be fluent in
spoken and written English.  The PhD studentship consists of an annual
bursary up to a maximum of three and a half years. In addition, you
will receive a desktop computer and conference allowance.

To apply for this position, you must have a strong background in at
least one of the following areas:

* Programming Languages
* Type Systems
* Formal Methods and Theories
* Systems

The starting date is 1st October 2019

Applications must include the following:

* A 2-page research statement that describes:

 (i) what you see as an interesting research issue;
 (ii) an outline of the objectives and methodology for the research;
 (iii) what relevant experience you have


*A detailed CV
*Transcripts of all degree results
*The contact details for two referees

Please email your application to <n.yoshida at imperial.ac.uk>
with the subject title "VeTSS PhD Scholarship on Session Types"

________________________________

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20190606/9b7f45ce/attachment-0001.html>