We are recruiting one PhD student to work on design and
implementation of programming languages. The post is on the project
TypeScript, The Next Generation,
and is funded by a
Microsoft Research PhD Scholarship.
There is increasing interest in integrating dynamically and statically
typed programming languages, as witnessed in industry by the
development of the languages TypeScript and Dart, and in academia by
the development of the theories of gradual types, hybrid types, and
the blame calculus. The purpose of our project is to bring the academic
and industrial developments together, applying theory to improve practice.
Our project focusses on JavaScript, an ECMA standard, and its typed
variant TypeScript, an open-source project sponsored by Microsoft.
JavaScript plays a central role in web-based applications and the new
Windows 8 framework, and TypeScript is seeing rapid takeup, with over
150 JavaScript libraries now provided with TypeScript
declarations. Our project has two parts, one aimed at immediate
short-term application, and one aimed at fundamental long-term
research.
- TypeScript TNG
The short-term goal is to build a tool, TypeScript: The Next Generation
(or TypeScript TNG for short), that generates
wrapper code from TypeScript
import declarations to detect and
pinpoint type errors. A wrapper will accept any JavaScript value as
input, and either raise an error or return a value guaranteed to
satisfy the invariant associated with the corresponding type. In
particular, wrappers for generic types will assure surprisingly strong
guarantees, known as “theorems for free”. Our hypothesis is that
TypeScript TNG will aid debugging and increase reliablility of
TypeScript and JavaScript code.
- A wide-spectrum type system.
The long-term goal is to extend the foundations of the blame calculus to
support a wide-spectrum of type systems, ranging from dynamic types (as
in JavaScript or Racket) through generic types (as in F# or
Haskell) to dependent types (as in F* or Coq). Our hypothesis is
that a wide-spectrum type system will increase the utility of
dependent types, by allowing dynamic checks to be used as a fallback
when static validation is problematic.
The workplan is likely to be too ambitious for a single
PhD studentship. Which aspects are carried out will depend on
which seem the most promising as our work develops, and on the
abilities and desires of the student.
The successful candidate will join the
ABCD team, carrying out
a research programme investigating sesion types and web programming.
The project is jointly supervised by Andrew Gordon
of Microsoft Research Cambridge and the University of Edinburgh.
You should possess an undergraduate degree in a relevant area, or
being nearing completion of same, or have comparable experience. You
should have evidence of ability to undertake research and communicate
well. You should have a background in programming languages,
including type systems, and programming and software engineering
skills.
It is desirable for candidates to also have one or more of the
following: a combination of theoretical and practical skills;
experience of JavaScript or web programming; knowledge of dependent type
theory; or training in empirical measurement of programming tasks. We
especially welcome applications from women and minorities.
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.
The successful candidate will receive a studentship covering tuition
and subsistence. Students from the UK or EU are preferred.
Consult the University
of Edinburgh website for details of
how to apply.
If you are interested, please send an outline of your qualifications to:
Prof. Philip Wadler (
wadler@inf.ed.ac.uk).
