[TYPES] Postdoctoral Research Assistant position at University of Edinburgh

[Philip Wadler]

The School of Informatics, University of Edinburgh invites applications for
a postdoctoral research assistant on the SAGE project (Scoped and Gradual
Effects), funded by Huawei. The post will be for eighteen months.

We seek applicants at an international level of excellence.  The School of
Informatics at Edinburgh is among the strongest in the world, and Edinburgh
is known as a cultural centre providing a high quality of life.

If interested, please contact Prof. Philip Wadler <wadler at inf.ed.ac.uk>.
Full details are here
<https://urldefense.com/v3/__https://elxw.fa.em3.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_1001/job/2929/?utm_medium=jobshare__;!!IBzWLUs!FV56I-OMUnQZ85YJDE8oWTxv2s-uAhFEQITL5l6J3dVFfwecuXimKJvlLrarq3bEyRTf0lSgrxA$ >.
Applications close at 5pm on 14 January 2021.

The Opportunity:

In the early 2000s, Plotkin and Power introduced an approach to
computational effects in programming languages known as *algebraic effects*.
This approach has attracted a great deal of interest and further
development, including the introduction by Plotkin and Pretnar of *effect
handlers*. Several research languages, such as Eff, Frank, Koka, and Links,
support the use of algebraic effects. A few languages, including Multicore
O'Caml and WebAssembly, support specific algebraic effects, and we may see
general algebraic effects make their way into mainstream languages in the
future.

The proposed research has two focusses: (a) a simpler version of static
scoping for algebraic effect handlers, and (b) gradual types for algebraic
effect systems.

The former is a question of how to match an effect with its corresponding
handler. This issue arises when two effects have the same name, and you
expect the handler for one but invoke the handler for the other. Some
current solutions, like tunnelling and instance variables, are based on
lexical scoping. However, despite this insight, tunnelling and instance
variables are more complex than lexical binding of a variable to a value.
In particular, the type system needs to track that an effect does not
escape the scope of its surrounding handler (reminiscent of the funarg
problem with dynamic variable binding). Can we do better?

The latter is a question of how to integrate legacy code that lacks typed
effects with new code that supports typed effects. Usually, integration of
dynamically and statically typed languages is best explored in the context
of gradual types, which support running legacy code and new code in tandem.
To date there is only a tiny amount of work in the area of gradual types
for effects, and important aspects of algebraic effects, such as effect
handlers, have yet to be addressed. Overall, work to date on effect
handlers is often complex, and attention is required to where ideas can be
simplified, which is the ultimate objective of this project.

Your skills and attributes for success:


Essential
• PhD (or close to completion) in programming languages or a related
discipline.
• Expertise and experience in relevant areas, including lambda calculus,
type systems, and compilation.
• Ability to implement prototype language processors in O’Caml, Haskell, or
a related language.
• Excellence in written and oral communication, analytical, and time
management skills.
• Ability to collaborate with a team.

Desirable

• Published research in programming languages or a related field,
preferably in top-tier conferences.
• Experience in presenting at conferences or seminars.
• Knowledge of effect systems or gradual type systems.
• Experience with a proof assistant, such as Agda or Coq.
• Strong programming and software engineering skills.


.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. https://urldefense.com/v3/__http://homepages.inf.ed.ac.uk/wadler/__;!!IBzWLUs!FV56I-OMUnQZ85YJDE8oWTxv2s-uAhFEQITL5l6J3dVFfwecuXimKJvlLrarq3bEyRTfPGNw5IM$ 
-------------- next part --------------
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.