The Coq mailing list

[Scott Owens <S.A.Owens AT kent.ac.uk>]

I’m presently looking (with Simon Thompson) for two Post Docs to work on a 
CakeML related project. (Although the CakeML verified compiler is developed 
in HOL4, rather than Coq, it is the same kind of verification project that is 
very common in the Coq world too.) The posts last for 3.5 years and are at 
the University of Kent in Canterbury, England. Applications are due by *12 
June, 2016*.

Here is a brief description of the project:

Trustworthy Refactoring project: Research Associate Positions in Refactoring 
Functional Programs and Formal Verification (for CakeML) 

The Trustworthy Refactoring project at the University of Kent is seeking to 
recruit postdoc research associates for two 3.5 year positions, to start in 
September this year.

The overall goal of this project is to make a step change in the practice of 
refactoring by designing and constructing of trustworthy refactoring tools. 
By this we mean that when refactorings are performed, the tools will provide 
strong evidence that the refactoring has not changed the behaviour of the 
code, built on a solid theoretical understanding of the semantics of the 
language. Our approach will provide different levels of assurance from the 
(strongest) case of a fully formal proof that a refactoring can be trusted to 
work on all programs, given some pre-conditions, to other, more generally 
applicable guarantees, that a refactoring applied to a particular program 
does not change the behaviour of that program. 

The project will make both theoretical and practical advances. We will build 
a fully-verified refactoring tool for a relatively simple, but full featured 
programming language (CakeML https://cakeml.org), and at the other we will 
build an industrial-strength refactoring tool for a related 
industrially-relevant language (OCaml). This OCaml tool will allow us to 
explore a range of verification techniques, both fully and partially 
automated, and will set a new benchmark for building refactoring tools for 
programming languages in general. 

The project, which is coordinated by Prof Simon Thompson and Dr Scott Owens, 
will support two research associates, and the four will work as a team. One 
post will focus on pushing the boundaries of trustworthy refactoring via 
mechanised proof for refactorings in CakeML, and the other post will 
concentrate on building an industrial strength refactoring tool for OCaml. 
The project has industrial support from Jane Street Capital, who will 
contribute not only ideas to the project but also host the second RA for a 
period working in their London office, understanding the OCaml infrastructure 
and their refactoring requirements.

You are encouraged to contact either of the project investigators by email 
(s.a.owens AT kent.ac.uk,
 
s.j.thompson AT kent.ac.uk)
 if you have any further questions about the post, or if you would like a 
copy of the full research application for the project. We expect that 
applicants will have PhD degree in computer science (or a related discipline) 
or be close to completing one. For both posts we expect that applicants will 
have experience of writing functional programs, and for the verification post 
we also expect experience of developing (informal) proofs in a mathematical 
or programming context.

To apply, please go to the following web pages:

Research Associate in Formal Verification for CakeML (STM0682): 

https://jobs.kent.ac.uk/fe/tpl_kent01.asp?s=4A515F4E5A565B1A&jobid=40106,3472764668&key=47167934&c=549534472123&pagestamp=sejmwzlocjpwfyyfak

Research Associate in Refactoring Functional Programs (STM0683): 

https://jobs.kent.ac.uk/fe/tpl_kent01.asp?s=4A515F4E5A565B1A&jobid=40107,6987525698&key=47167934&c=549534472123&pagestamp=sesioeandjktfucacs

Simon and Scott