From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 418B97FD90 for ; Thu, 12 Jan 2017 19:29:31 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=p.m.sewell@googlemail.com; spf=Pass smtp.mailfrom=p.m.sewell@googlemail.com; spf=None smtp.helo=postmaster@mail-qt0-f175.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of p.m.sewell@googlemail.com) identity=pra; client-ip=209.85.216.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="p.m.sewell@googlemail.com"; x-sender="p.m.sewell@googlemail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of p.m.sewell@googlemail.com designates 209.85.216.175 as permitted sender) identity=mailfrom; client-ip=209.85.216.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="p.m.sewell@googlemail.com"; x-sender="p.m.sewell@googlemail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qt0-f175.google.com) identity=helo; client-ip=209.85.216.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="p.m.sewell@googlemail.com"; x-sender="postmaster@mail-qt0-f175.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ArVsMwxH4wbm5Bhm33MhKRp1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ7zpc+wAkXT6L1XgUPTWs2DsrQf2raQ6PirADVcqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRo?= =?us-ascii?q?LerpBIHSk9631+ev8JHPfglEnjSwbLd9IRmsowjdqsYajZZ/Jqs+1xDEvmZGd+?= =?us-ascii?q?NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLD?= =?us-ascii?q?TRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljj?= =?us-ascii?q?oMOjgk+2/Vl8NwlrpWrxCvpxJ/zYDaY5ybOuRica7GZ9wWWXBMU9xNWyBdAI6x?= =?us-ascii?q?aZYEAeobPeZfqonwv0EAogWiBQayHuPk1yJGiWH43KIk1+QhFRzN0Qs6Ed0QrH?= =?us-ascii?q?Tbss/1OL0PX++rwqjH0zHDb/dN1Djh7IjEaAwuruuJXb5qa8Xe1VMjFx7GjliJ?= =?us-ascii?q?r4HuIj2b1uMIs2eB7upgU/qii3Q5pAF0uTij3MYsio7Rio0J0F/E8D91z5wpKt?= =?us-ascii?q?GiVU57YtipG4ZTuSGCL4Z6XN8uTmVytCs5yrAKo4C3cDULxZg92hLSafyKfo6V?= =?us-ascii?q?6Rz5TumROy13hHd9dbK/mRmy9U+gx/X5Vsau0VZKqjNJksDQtnwRzhDT5NWLR/?= =?us-ascii?q?l980u71jaP0AfT6u5AIU8qj6bUN5khwrsompoSt0TMADP2lV3ogKOKckgo4Oul?= =?us-ascii?q?5uT9brn4u5ORNpV4hhz8P6kugsC/BP43MgkKX2iV4+S807jj8FXhQLlQi/06iL?= =?us-ascii?q?LZv47UJMsFoq65BxRY0okk6xa4ADem1MoXnXwdI1JEfBKLlZTmO1bLIPzgF/ew?= =?us-ascii?q?n0yskCt3x/DBJrDuHo/CLn3HkLv4ebZ96lVcyBYowNBE55NUD6kBL+jpVk/wst?= =?us-ascii?q?zYFB45PBauz+bpEtUunr8ZDGmGB6vcNKLJrXeJ4PguKq+CftwvtS75OsQissbj?= =?us-ascii?q?kXIj32QQYqSt2bMcbDazF/EgKk7ffHm/rM0GFDIysxYzVqTRhUKPVTobM06/Q6?= =?us-ascii?q?8moAo2F4+iCa/IQsamibnH1Sz9A54ANTMOMUyFDXq9L9bMYPwLci/HesI=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0C2BgAUyndYhq/YVdFdFgcBBQELARgBB?= =?us-ascii?q?QELAYMRAQEBAQFvD4EJB4NJnByCO5R9KYJCgzaCAQdCEQEBAQEBAQEBAQEBEgE?= =?us-ascii?q?BAQgLCwodMIIzGYIeAQMBASMdARIYBwgDDAEFBQsHGxUCAiISAQUBDg4ZiGUDE?= =?us-ascii?q?AgOpDM/imOBIIFLBVWDCQWBWoIvJw0rGoIQAR0CBhKGM4RhgmmBQ0cSgg0MLoI?= =?us-ascii?q?/HwWbLIZbinuBd1GEPYlljlGCTRQegRQ1gTcSLlIFgQOBQIEgKYIKPjUBAYYpK?= =?us-ascii?q?4IQAQEB?= X-IPAS-Result: =?us-ascii?q?A0C2BgAUyndYhq/YVdFdFgcBBQELARgBBQELAYMRAQEBAQF?= =?us-ascii?q?vD4EJB4NJnByCO5R9KYJCgzaCAQdCEQEBAQEBAQEBAQEBEgEBAQgLCwodMIIzG?= =?us-ascii?q?YIeAQMBASMdARIYBwgDDAEFBQsHGxUCAiISAQUBDg4ZiGUDEAgOpDM/imOBIIF?= =?us-ascii?q?LBVWDCQWBWoIvJw0rGoIQAR0CBhKGM4RhgmmBQ0cSgg0MLoI/HwWbLIZbinuBd?= =?us-ascii?q?1GEPYlljlGCTRQegRQ1gTcSLlIFgQOBQIEgKYIKPjUBAYYpK4IQAQEB?= X-IronPort-AV: E=Sophos;i="5.33,219,1477954800"; d="scan'208,217";a="208947459" Received: from mail-qt0-f175.google.com ([209.85.216.175]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 12 Jan 2017 19:29:28 +0100 Received: by mail-qt0-f175.google.com with SMTP id k15so26107797qtg.3 for ; Thu, 12 Jan 2017 10:29:28 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20161025; h=mime-version:reply-to:sender:in-reply-to:references:from:date :message-id:subject:to; bh=Lp6PrXIRWATQ0PkqLf1ODCfX8tC9Ia/BJ3TU2l0ZqTQ=; b=MhhRBqJ3yIOBvYwMoVCvpon/eA2MwuMkJM3JXT766ecoKRloDbs0VpUnHn4FccZ02u BqDO2jZFeIrdXq5K2/Z98JvmWRR8ISK8jkFlazUAJ52Ts0QsygfIPCrb3p2Mj2RanzEk Q6vRCEK+QT/OnXniNgwRQcaa48UzWuFxttcSO+WzC+GN4Scg8QDczM4bmB19knz7xWx9 ugOS4YEsqjl0O3D+dLvxEziH0avBrDd8Nrkq4vfXRdqFFmh3zYFYG2BEXeKxe46KCJB+ 2TmJ84Tw+Ly/Kqxsp95oRwqvafS+g1IPKYgamdRe1MR34Mmiqm7XKow1XFImm2MjuwgB 0XpA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:reply-to:sender:in-reply-to :references:from:date:message-id:subject:to; bh=Lp6PrXIRWATQ0PkqLf1ODCfX8tC9Ia/BJ3TU2l0ZqTQ=; b=KyMRQu7xjupfjUnJhX7crYYietlj/+MpIDVd6ml/3fNt8MSaQroJhAf8bMog6xSuIC /6gY0bh19jN1HHJSZrwZ1jx07O6wWmRJ/cOxYlUt2vxKQXql94UkTcT7J/0bZTH6/VxV OH9Xxa0xWMwBLBwmJjoqTq8TxyIQSBIY/sJo4venDtQM+4RCTHC2/8RsqCkqiML/MH1H kEYFOhXD1doBoAsHtBTgu2NC/WSUUcr+YMVCnkf0lNsR+gMR4HyKLaJKN6z25sOitmPp JD+3lxurvmUGeX10sKSGHa2v70tPsMMdIQoced3D6JOY5JcGksoj75tsft7e+W/rA6nZ PAbA== X-Gm-Message-State: AIkVDXK9SWzWaFhZKjyIy0VHSqxZwQOIgwdV7ckppXTmEiAXlBYrBLSJ7Zl2/yiRlf3zLXWjoo44YsE0NaEO4Q== X-Received: by 10.237.42.108 with SMTP id k41mr13476415qtf.81.1484245767110; Thu, 12 Jan 2017 10:29:27 -0800 (PST) MIME-Version: 1.0 Reply-To: Peter.Sewell@cl.cam.ac.uk Sender: p.m.sewell@googlemail.com Received: by 10.12.160.98 with HTTP; Thu, 12 Jan 2017 10:29:26 -0800 (PST) In-Reply-To: References: From: Peter Sewell Date: Thu, 12 Jan 2017 18:29:26 +0000 X-Google-Sender-Auth: 52un31cNKqCf1J2m1WKFrZ3Dny0 Message-ID: To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=001a113d463cb55ea90545e9e500 Subject: Re: [Caml-list] Postdoc position in Applied Semantics for Production Architectures --001a113d463cb55ea90545e9e500 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On 15 December 2016 at 23:23, Peter Sewell wrote: > [please circulate this to any likely candidates - thanks, Peter] > > Research Associate/Senior Research Associate in Applied Semantics for > Production Architectures > Updating this: the likellihood of new funding means we may be able to make several appointments, to build a really strong team. Closing date 24 Jan, as before. Peter > > University of Cambridge Computer Laboratory > Research Associate =C2=A329,301 - =C2=A338,183 or Senior Research Associa= te =C2=A339,324 > - 49,772 > Fixed-term: until February 28, 2019, when the grant funding the post > currently ends. > Details: http://www.jobs.cam.ac.uk/job/12397/ > > > Do you want to help build mathematically rigorous foundations for > real-world computing, to make it more robust and secure? > > We have an ongoing project to establish rigorous semantic models for > production multiprocessors, to provide a clear basis for programming, > software verification, and hardware verification. This involves long-term > close collaborations with ARM and IBM, and we have an agreement with ARM = to > take their internal ISA description, build a mathematical model based on > it, integrate it with the concurrency semantics we are developing, and > release the whole in a form usable for verification. This will provide the > first strongly validated public model for a production multiprocessor > architecture. We also have a close collaboration with the CHERI research > project, developing processors with hardware-accelerated in-process memory > protection and sandboxing, together with an open-source operating system > and toolchain based on FreeBSD and Clang/LLVM; formal modelling is at the > heart of the CHERI design process. For more details, see some of our > previous papers: > POPL17 (http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf), POPL16 ( > http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf), MICRO 2015 ( > http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf), PLDI11 ( > http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf), > CHERI ISA spec (http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.html), > CHERI (https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/), REMS ( > http://rems.io). > > We have a position available to work on: > > - the development of our Sail metalanguage for ISA description: a language > with a lightweight dependent type system, designed to capture ARM, IBM > POWER, and CHERI instruction semantics in an engineer-friendly way; > - translation from Sail to generate efficient emulators and usable > theorem-prover definitions; > - mechanised proof about the architecture definitions, e.g. of security > properties, relationships between concurrency models, and correctness > results for high-level language concurrency compilation; and/or > - development of reasoning, symbolic execution, debugging, and/or > model-checking tools above the architecture definitions - the initial work > should generate many opportunities along these lines. > > The successful candidate must have a PhD (or equivalent experience), a > track-record of publication in relevant areas of Computer Science, good > knowledge of English and communication skills, and the expertise and > commitment to apply rigorous semantics to real systems. We're looking for > people with the skills to make solid models and tools, well-engineered and > widely usable. You should have expertise in one or more of: > > - functional programming (e.g. OCaml) > - programming language semantics and type systems > - theorem provers, especially Isabelle and/or Coq > - symbolic execution > - model-checking > > For senior applicants, e.g. who will be able to contribute substantially > to future grant applications, it may be possible to appoint at the Senior > Research Associate level. > > This is part of the broader REMS (Rigorous Engineering for Mainstream > Systems) programme grant: a lively collaboration between systems and > semantics researchers in Cambridge, Imperial, and Edinburgh to scale up a= nd > apply mathematically rigorous semantics to mainstream systems. > > Informal enquiries should be directed to Peter Sewell ( > Peter.Sewell@cl.cam.ac.uk). > > To apply online for this vacancy, please click on the 'Apply' button > below. This will route you to the University's Web Recruitment System, > where you will need to register an account (if you have not already) and > log in before completing the online application form. > > Please ensure you upload your Curriculum Vitae (CV) and a cover letter > explaining your potential contribution to the project, as pdf documents. > Include the names of 2 or 3 referees at the appropriate point in the onli= ne > application. Your referees should be prepared to send references within a > week of the closing date, if asked by the University. If you upload any > additional documents which have not been requested, we will not be able to > consider these as part of your application. > > Please quote reference NR10978 on your application and in any > correspondence about this vacancy. > > The University values diversity and is committed to equality of > opportunity. > > The University has a responsibility to ensure that all employees are > eligible to live and work in the UK. > > --001a113d463cb55ea90545e9e500 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable


On 15 December 2016 at 23:23, Peter Sewell <Peter.Sewell@cl.ca= m.ac.uk> wrote:
[please circulate this to any likely candidates - = thanks, Peter]

Research Associate/Senior Research Associate in Appli= ed Semantics for Production Architectures

Updating this: the likellihood of new funding means we may be able=20 to make several appointments, to build a really strong team.=C2=A0=C2=A0 Cl= osing=20 date 24 Jan, as before.
=C2=A0
Peter
=
=C2=A0

University of Cambridge Computer Laboratory
Research Associ= ate =C2=A329,301 - =C2=A338,183 or Senior Research Associate =C2=A339,324 -= 49,772
Fixed-term: until February 28, 2019, when the grant funding the = post currently ends.
Details: http://www.jobs.cam.ac.uk/job/12397/
<= br>
Do you want to help build mathematically rigorous foundations for re= al-world computing, to make it more robust and secure?

We have an on= going project to establish rigorous semantic models for production multipro= cessors, to provide a clear basis for programming, software verification, a= nd hardware verification. This involves long-term close collaborations with= ARM and IBM, and we have an agreement with ARM to take their internal ISA = description, build a mathematical model based on it, integrate it with the = concurrency semantics we are developing, and release the whole in a form us= able for verification. This will provide the first strongly validated publi= c model for a production multiprocessor architecture. We also have a close = collaboration with the CHERI research project, developing processors with h= ardware-accelerated in-process memory protection and sandboxing, together w= ith an open-source operating system and toolchain based on FreeBSD and Clan= g/LLVM; formal modelling is at the heart of the CHERI design process. For m= ore details, see some of our previous papers:
POPL17 (http://w= ww.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf), POPL16 (ht= tp://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf), MICRO 2015 (http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf), PLDI11 (http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/<= wbr>pldi105-sarkar.pdf), CHERI ISA spec (http://www.cl.cam.a= c.uk/techreports/UCAM-CL-TR-891.html), CHERI (http= s://www.cl.cam.ac.uk/research/security/ctsrd/cheri/), REMS (<= a href=3D"http://rems.io" target=3D"_blank">http://rems.io).

We = have a position available to work on:

- the development of our Sail = metalanguage for ISA description: a language with a lightweight dependent t= ype system, designed to capture ARM, IBM POWER, and CHERI instruction seman= tics in an engineer-friendly way;
- translation from Sail to generate ef= ficient emulators and usable theorem-prover definitions;
- mechanised pr= oof about the architecture definitions, e.g. of security properties, relati= onships between concurrency models, and correctness results for high-level = language concurrency compilation; and/or
- development of reasoning, sym= bolic execution, debugging, and/or model-checking tools above the architect= ure definitions - the initial work should generate many opportunities along= these lines.

The successful candidate must have a PhD (or equivalen= t experience), a track-record of publication in relevant areas of Computer = Science, good knowledge of English and communication skills, and the expert= ise and commitment to apply rigorous semantics to real systems. We're l= ooking for people with the skills to make solid models and tools, well-engi= neered and widely usable. You should have expertise in one or more of:
<= br>- functional programming (e.g. OCaml)
- programming language semantic= s and type systems
- theorem provers, especially Isabelle and/or Coq
= - symbolic execution
- model-checking

For senior applicants, e.g.= who will be able to contribute substantially to future grant applications,= it may be possible to appoint at the Senior Research Associate level.
<= br>This is part of the broader REMS (Rigorous Engineering for Mainstream Sy= stems) programme grant: a lively collaboration between systems and semantic= s researchers in Cambridge, Imperial, and Edinburgh to scale up and apply m= athematically rigorous semantics to mainstream systems.

Informal enq= uiries should be directed to Peter Sewell (Peter.Sewell@cl.cam.ac.uk).

To ap= ply online for this vacancy, please click on the 'Apply' button bel= ow. This will route you to the University's Web Recruitment System, whe= re you will need to register an account (if you have not already) and log i= n before completing the online application form.

Please ensure you u= pload your Curriculum Vitae (CV) and a cover letter explaining your potenti= al contribution to the project, as pdf documents. Include the names of 2 or= 3 referees at the appropriate point in the online application. Your refere= es should be prepared to send references within a week of the closing date,= if asked by the University. If you upload any additional documents which h= ave not been requested, we will not be able to consider these as part of yo= ur application.

Please quote reference NR10978 on your application a= nd in any correspondence about this vacancy.

The University values d= iversity and is committed to equality of opportunity.

The University= has a responsibility to ensure that all employees are eligible to live and= work in the UK.


--001a113d463cb55ea90545e9e500--