From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 56D1D7FD92 for ; Tue, 7 Jun 2016 16:14:49 +0200 (CEST) IronPort-PHdr: 9a23:WHxREBOR0fy4xtPK/Mkl6mtUPXoX/o7sNwtQ0KIMzox0KPv5rarrMEGX3/hxlliBBdydsKIVzbWP+P6xEUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35XxiLn5pcybSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskzIRA6Lri8XW2AS1x5JGBTt7RfgX563vDGs5cRn3yzPBszzSrZ8EQii6KJzUxjuwHMccTx/7GHQj9Rri6Rzox+nu1p2yMjJY9fGZ7JFYqrBcIZCFiJ6VcFLWnkEW9vkYg== Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=s.j.thompson@kent.ac.uk; spf=None smtp.mailfrom=s.j.thompson@kent.ac.uk; spf=None smtp.helo=postmaster@mx2.kent.ac.uk Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of s.j.thompson@kent.ac.uk) identity=pra; client-ip=129.12.21.33; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="s.j.thompson@kent.ac.uk"; x-sender="s.j.thompson@kent.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of s.j.thompson@kent.ac.uk) identity=mailfrom; client-ip=129.12.21.33; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="s.j.thompson@kent.ac.uk"; x-sender="s.j.thompson@kent.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mx2.kent.ac.uk) identity=helo; client-ip=129.12.21.33; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="s.j.thompson@kent.ac.uk"; x-sender="postmaster@mx2.kent.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DQAgAF1lZXfiEVDIFdFoN9fbxhFwaFdoE8PBABAQEBAQEBAREBAQsLCQkhL4IwglYPMIE+E4gvDrhxg0gBAQEBAQEEAQEBAQEBAQEBAR2IHoFpgiaCWQ4DAYJlC0AYghIcBZhLgTGEU4gjgWqEUohkiAmHVjWCMyWBNm0BiFmBNQEBAQ X-IPAS-Result: A0DQAgAF1lZXfiEVDIFdFoN9fbxhFwaFdoE8PBABAQEBAQEBAREBAQsLCQkhL4IwglYPMIE+E4gvDrhxg0gBAQEBAQEEAQEBAQEBAQEBAR2IHoFpgiaCWQ4DAYJlC0AYghIcBZhLgTGEU4gjgWqEUohkiAmHVjWCMyWBNm0BiFmBNQEBAQ X-IronPort-AV: E=Sophos;i="5.26,433,1459807200"; d="scan'208";a="180468457" Received: from mx2.kent.ac.uk ([129.12.21.33]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 07 Jun 2016 16:14:48 +0200 Received: from edu7018.kent.ac.uk ([129.12.112.24]) by mx2.kent.ac.uk with esmtpsa (TLSv1:AES256-SHA:256) (Exim 4.72) (envelope-from ) id 1bAHmJ-0003CX-Ky; Tue, 07 Jun 2016 15:14:47 +0100 From: Simon Thompson Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: quoted-printable Date: Tue, 7 Jun 2016 15:14:47 +0100 Message-Id: <910A0C0A-5DF7-430F-A5C7-FF74AF9704E6@kent.ac.uk> Cc: Scott Owens To: caml Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) X-Mailer: Apple Mail (2.3124) Subject: [Caml-list] Verified refactoring in OCaml and CakeML: 2 postdoc positions: closes 13-June-2016 The Trustworthy Refactoring project at the University of Kent is seeking to= recruit postdoc research associates for two 3.5 year positions, to start i= n September this year. The overall goal of this project is to make a step change in the practice o= f refactoring by designing and constructing of trustworthy refactoring tool= s. By this we mean that when refactorings are performed, the tools will pro= vide strong evidence that the refactoring has not changed the behaviour of = the code, built on a solid theoretical understanding of the semantics of th= e language. Our approach will provide different levels of assurance from th= e (strongest) case of a fully formal proof that a refactoring can be truste= d to work on all programs, given some pre-conditions, to other, more genera= lly applicable guarantees, that a refactoring applied to a particular progr= am does not change the behaviour of that program.=20 The project will make both theoretical and practical advances. We will buil= d a fully-verified refactoring tool for a relatively simple, but full featu= red programming language (CakeML https://cakeml.org), and at the other we w= ill build an industrial-strength refactoring tool for a related industriall= y-relevant language (OCaml). This OCaml tool will allow us to explore a ran= ge of verification techniques, both fully and partially automated, and will= set a new benchmark for building refactoring tools for programming languag= es in general.=20 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. O= ne post will focus on pushing the boundaries of trustworthy refactoring via= mechanised proof for refactorings in CakeML, and the other post will conce= ntrate on building an industrial strength refactoring tool for OCaml. The p= roject 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 wor= king in their London office, understanding the OCaml infrastructure and the= ir refactoring requirements. You are encouraged to contact either of the project investigators by email = (s.a.owens@kent.ac.uk, s.j.thompson@kent.ac.uk) if you have any further que= stions about the post, or if you would like a copy of the full research app= lication 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 fu= nctional 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):=20 https://jobs.kent.ac.uk/fe/tpl_kent01.asp?s=3D4A515F4E5A565B1A&jobid=3D4010= 6,3472764668&key=3D47167934&c=3D549534472123&pagestamp=3Dsejmwzlocjpwfyyfak Research Associate in Refactoring Functional Programs (STM0683):=20 https://jobs.kent.ac.uk/fe/tpl_kent01.asp?s=3D4A515F4E5A565B1A&jobid=3D4010= 7,6987525698&key=3D47167934&c=3D549534472123&pagestamp=3Dsesioeandjktfucacs Simon and Scott Simon Thompson | Professor of Logic and Computation=20 School of Computing | University of Kent | Canterbury, CT2 7NF, UK s.j.thompson@kent.ac.uk | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt