The Coq mailing list

[Sergio Maffeis <maffeis AT doc.ic.ac.uk>]

One Postdoctoral Researcher position (RA) is available in the Department 
of Computing at Imperial College London.


JavaScript is pervasive in most web applications. JavaScript 
applications can be programmed directly, or can be obtained by compiling 
from other languages. Either way, a rigorous model of JavaScript is 
invaluable to develop trustworthy analyses of web programs. The JSCert 
project (http://jscert.org) has developed a mechanised specification of 
JavaScript in the Coq proof assistant, and a corresponding reference 
interpreter for JavaScript in OCaml, provably correct and thoroughly 
tested.


The post-doctoral researcher, leveraging (and contributing to) the 
JSCert infrastructure, will work on some combination of:

- Security: information flow control, secure subsets, defence against 
web vulnerabilities;
- Verification: static/dynamic analysis tools for guaranteeing safety or 
finding bugs;
- Compilation: translation from other languages into JavaScript, from 
JavaScript to bytecode or asm.js.

JScert is a collaboration between Imperial College and INRIA. The 
position will be based in London, but will offer significant scope of 
collaboration with various INRIA sites.


The position is for up to 3 years, starting as soon as possible. The 
salary is in the range 32k - 41k GBP (depending on experience) plus a 
budget for travel and equipment. Imperial College is in the heart of 
London, close to beautiful parks, good restaurants, cultural attractions 
and entertainment venues. Candidates must hold a PhD, should have a 
strong track record in formal methods, and an interest in some of: proof 
assistants, development of verification tools, static analyses, web 
security.


For inquiries please contact Dr Sergio Maffeis 
(maffeis AT doc.ic.ac.uk).