[TYPES/announce] Microsoft Research PhD Scholarship: TypeScript, The Next Generation

[Philip Wadler]

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<http://blogs.msdn.com/b/msr_er/archive/2014/02/28/2014-microsoft-research-phd-scholarship-projects-announced.aspx>.


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<http://groups.inf.ed.ac.uk/abcd/>,
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<http://www.ed.ac.uk/schools-departments/informatics/postgraduate/apply/overview>.


If you are interested, please send an outline of your qualifications to:
Prof. Philip Wadler (wadler at inf.ed.ac.uk).

http://homepages.inf.ed.ac.uk/wadler/typescript-tng-phd-advert.html
.   \ Philip Wadler, Professor of Theoretical Computer Science
.   /\ School of Informatics, University of Edinburgh
.  /  \ http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20140311/f8e6fffe/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20140311/f8e6fffe/attachment.ksh>