Wadler's Blog

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).

Labels: Dynamic and Static Typing, Edinburgh, Functional Programming, JavaScript, Programming Languages, Types