[TYPES/announce] Post-Doc and PhD positions at Edinburgh, Glasgow, and Imperial

[Philip Wadler]

--------------------------------------------------------------------------
>From Data Types to Session Types: A Basis for Concurrency and Distribution
--------------------------------------------------------------------------

              Post-Doc and PhD positions
         at Edinburgh University, Glasgow University,
             and Imperial College London

We will soon be recruiting for a number of post-doc positions and PhD
studentships on a new project funded by EPSRC, the UK science funding
agency. The title of the project is "From Data Types to Session Types:
A Basis for Concurrency and Distribution", and its goal is to further
develop the theory and practice of session types for structuring
concurrent and distributed software.

The project has particular emphasis on putting theory into practice,
by embedding session types in a range of programming languages and
applying them to realistic case studies.  The research programme
includes collaboration with Amazon, Cognizant, Red Hat, VMware, and
the NSF-funded Ocean Observatories Initiative. A brief summary of the
project is reproduced at the end of this message.

The project is funded for 5 years from 1st June 2013. The following
positions will be available:

  School of Informatics, University of Edinburgh: 1 post-doc, 1 PhD

  School of Computing Science, University of Glasgow: 2 post-docs, 1 PhD

  Department of Computing, Imperial College London: 2 post-docs, 1 PhD

Post-doc positions will be for an initial period of 2 years, from 1st
June or as soon as possible thereafter, with the possibility of
extension. PhD studentships will be for 3.5 years from 1st October
(available to UK/EU residents only). There will be a further 3 PhD
studentships, one at each university, from 1st October 2014.

Candidates for the post-doc positions will need to have expertise in
programming language design (including formal semantics and type
theory) and implementation. Different positions will be suitable for
different points on the theory/practice spectrum. We will be
especially interested in candidates with a combination of theoretical
and practical skills. PhD candidates should have an interest in the
same topics.

We seek applicants at an international level of excellence.
The computing departments at Edinburgh, Glasgow, and Imperial are
among the strongest in the world, and Edinburgh, Glasgow, and London
are known as cultural centres providing a high quality of life.

The positions have not yet been set up within the universities'
recruitment systems, but we are announcing them now so that interested
candidates can contact us informally. We will send a second advert
with full details of how to apply, deadlines, salaries, employment
conditions, etc, as soon as possible.

Anyone interested in either the post-doc positions or the PhD
studentships is invited to contact the investigators:

Philip Wadler, University of Edinburgh
(wadler at inf.ed.ac.uk)

Simon Gay, University of Glasgow
(Simon.Gay at glasgow.ac.uk)

Nobuko Yoshida, Imperial College London
(N.Yoshida at imperial.ac.uk)

----------------------
Summary of the Project
----------------------

We aim to solve computing's most pressing problem - concurrency and
distribution - by adapting computing's most successful solution - the
data type. Data types codify the structure of data; session types
codify the structure of communication. Session types will enable a
revolution in the development of concurrent and distributed software,
making it cheaper to construct and maintain, and more reliable.

Concurrency and distribution are computing's most pressing problem:
unless we discover a way to routinely and reliably build concurrent
and distributed systems, a half century of unprecedented technical
progress will draw to a close. We are approaching the 50th anniversary
of Moore's Law, the observation that component counts and clock speeds
double every 18 months. No exponential improvement can continue
forever, and recently this rule has changed: clock speeds now remain
fixed while the number of processors doubles, so exploitation of
concurrency is essential. Meanwhile, everyone now has a computer in
their pocket, and these computers depend crucially on communication to
achieve their function. We inhabit a world of web applications, cloud
services, and mobile apps: society increasingly depends on a
technological infrastructure of concurrent and distributed systems.

Programming concurrent and distributed systems is notoriously
difficult. Many solutions are based on shared memory, which requires
the programmer to reason about every possible interleaving by which
many processors access a common resource. Shared memory scales only to
a certain point; it is not appropriate for programming the server
farms that drive the web or for mobile applications. The most
successful solutions so far appear to be those that replace shared
memory with communication as the central structuring
technique. Communication usually centres around the notion of a
protocol, a series of operations in a specific order. However, direct
support for protocols at the language level has been lacking, as
compared with data types.

The data type is computing's most successful solution. Data types
appear from the oldest programming language to the newest, and cover
concepts ranging from a single byte to organised tables containing
information on customers and orders. Types act as the fundamental unit
of compositionality: the first thing a programmer writes or reads
about each method is its data type, and type discipline guarantees
that each call of a method matches its definition. Data types play a
central role in all aspects of software, from architectural design to
interactive development environments to efficient compilation.

The analogue of the data type for concurrency and distribution is the
session type. A session type codifies the notion of a protocol.
Session types build on data types, as data types specify the lowest
level of data exchange, upon which more complex protocols are
built. Just as type discipline matches use and definition of a method,
so session types ensure consistency between the two ends of a
communication.

We expect session types to play a role in all aspects of
software. Today, architects discuss the high-level structure of a
system in terms of its types, but must resort to informal notions of
protocol to describe communication; in future, they will describe
communication in terms of session types. Today, programmers use tools
that let them search for methods and modules based on their type, and
give immediate feedback if their program violates type discipline, but
must resort to informal notions of protocol when coding
communications; in future, they will search for components based on
their session type, and get immediate feedback if their program
violates session type discipline. Today, software tools exploit types
to optimise code, but cannot exploit the informal notions of protocol
to optimise communication; in future, communication middleware will
exploit session types to support efficient messaging.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20130228/451771ad/attachment-0001.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20130228/451771ad/attachment-0001.ksh>