From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 301967FD90 for ; Fri, 16 Dec 2016 00:23:51 +0100 (CET) Authentication-Results: mail2-smtp-roc.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-wm0-f49.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of p.m.sewell@googlemail.com) identity=pra; client-ip=74.125.82.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="p.m.sewell@googlemail.com"; x-sender="p.m.sewell@googlemail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of p.m.sewell@googlemail.com designates 74.125.82.49 as permitted sender) identity=mailfrom; client-ip=74.125.82.49; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wm0-f49.google.com) identity=helo; client-ip=74.125.82.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="p.m.sewell@googlemail.com"; x-sender="postmaster@mail-wm0-f49.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3A3hfbWBRHwpD5k7GEdVsd0poSp9psv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa64ZRWN2/xhgRfzUJnB7Loc0qyN4vumBjRLuMzJ8ChbNscTB1ld0Y?= =?us-ascii?q?RetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1o?= =?us-ascii?q?Ora9QdaK3Izkn9y1rpbaZgENgDumfZtzKg+3pEPfrJosjJNmO5o2nyPEvnZSPd?= =?us-ascii?q?9b2m5sIXqYm1D378L29ZUl7icDlegm8pt4XLn3ZewDQKNVCDBuZ1g4+MDx8yLO?= =?us-ascii?q?UgaL4lMXViMdmx8OCgOD8RKsDcS5iTfzqucogHrSBsbxV71hATk=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DHAQDtJFNYhjFSfUpdFjIGDIMNAQEBA?= =?us-ascii?q?QE/LA6BBgeFSqEOjS2FJIIKKYJCgVyBWoIFB0ESAQEBAQEBAQEBAQESAQEBCAs?= =?us-ascii?q?LCR0wQhKBXxiCIiUdARIYBwgDDQUQBxsVAiQSAQUBDieIUQMXDpkEgz8/g26Gd?= =?us-ascii?q?IEggUsFWIMNBYFZgiUnDSsagxYeAgYShiSHPIFDRxKCDQstgj8eBZprgUqFB4p?= =?us-ascii?q?igXRRhDCJVpBdFB6BFCUBgTFdA4FlgROCPz40AQGCdYM6K4IQAQEB?= X-IPAS-Result: =?us-ascii?q?A0DHAQDtJFNYhjFSfUpdFjIGDIMNAQEBAQE/LA6BBgeFSqE?= =?us-ascii?q?OjS2FJIIKKYJCgVyBWoIFB0ESAQEBAQEBAQEBAQESAQEBCAsLCR0wQhKBXxiCI?= =?us-ascii?q?iUdARIYBwgDDQUQBxsVAiQSAQUBDieIUQMXDpkEgz8/g26GdIEggUsFWIMNBYF?= =?us-ascii?q?ZgiUnDSsagxYeAgYShiSHPIFDRxKCDQstgj8eBZprgUqFB4pigXRRhDCJVpBdF?= =?us-ascii?q?B6BFCUBgTFdA4FlgROCPz40AQGCdYM6K4IQAQEB?= X-IronPort-AV: E=Sophos;i="5.33,354,1477954800"; d="scan'208,217";a="250299900" Received: from mail-wm0-f49.google.com ([74.125.82.49]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 16 Dec 2016 00:23:50 +0100 Received: by mail-wm0-f49.google.com with SMTP id g23so8520626wme.1 for ; Thu, 15 Dec 2016 15:23:50 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20161025; h=mime-version:reply-to:sender:from:date:message-id:subject:to; bh=EPcyMjGlSZz0bJVLUIslvyNOovgG9hTlMw9vM38Djss=; b=FssE6l9Kzty+uiZbOZNDnf05afgZUH0vwscvSCN8A17gwrnsYrwYTg8t9w+oTUvm+C cIdmarskfAT2Y8KnfWcrHateGRm4lhUWSbO8ttxbFSBUiz5G8DszEoIIEFK8pf4eoRnS Hleme0NvdZViZmjOejHzVDrLZC2P2VDaoI2bUQcxT0OCQ9QIW+3aYPFQohPi33pp63Su KM9T4Za9hQ6PywAH8jWlmUUCy4D8NgAVJMpjKV8EVgumXOHpdbD/WftF9zsU37A81L4X vWzlRbV8Y6KPc31y0ZDJguUENIlwqRD9BTPtJGbRWZfzHKN6NS/2BzUAgMuHgcVFUBqC iV4Q== 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:from:date :message-id:subject:to; bh=EPcyMjGlSZz0bJVLUIslvyNOovgG9hTlMw9vM38Djss=; b=kF/yUBOMbNQxlW4aSX7gI3/ZqeG/zgJ+WOalJEbRsVYNXjjjhU3E2N0HTnblfwV5PK s9PBaXMo/lvzIUG//hEXR/Il6nR+rSk/BHTFDHfq8TtaihMbEg5i01rZHZ0o8ICU2MG3 xeK9Ma8vMj5BpdscjsqhzlmyydXe67E/aoygva/G8zeacRSxhk2XJWL8BV1TG/gpnd3Z j+6eP5OdtL4yJ8QY6cemJjdUnG/sy3WZte4DGBDhayx8QPlOmHhtcYleIuQzNVvtxVXN RMJljlxrEb4gIVY1+a/PXSUovx4E8G4htiKeLRgX4UttDMDBXNJlao9Xqp5GNVOC9sIX RaVA== X-Gm-Message-State: AIkVDXK5+X+IT8CdPEpunlDhmxMqhYnokwCcHbCltUYtz9McPEelwfuZTK/04T/2v4Guso4NipFJE/KBknExjA== X-Received: by 10.28.4.199 with SMTP id 190mr552994wme.11.1481844229351; Thu, 15 Dec 2016 15:23:49 -0800 (PST) MIME-Version: 1.0 Reply-To: Peter.Sewell@cl.cam.ac.uk Sender: p.m.sewell@googlemail.com Received: by 10.28.103.9 with HTTP; Thu, 15 Dec 2016 15:23:48 -0800 (PST) From: Peter Sewell Date: Thu, 15 Dec 2016 23:23:48 +0000 X-Google-Sender-Auth: n3_GgKekcnWbVL10sSDzj4Qpda8 Message-ID: To: caml-list@inria.fr Content-Type: multipart/alternative; boundary=001a1141e304e72e1d0543babe16 Subject: [Caml-list] Postdoc position in Applied Semantics for Production Architectures --001a1141e304e72e1d0543babe16 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable [please circulate this to any likely candidates - thanks, Peter] Research Associate/Senior Research Associate in Applied Semantics for Production Architectures University of Cambridge Computer Laboratory Research Associate =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/ 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 and 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 online 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. --001a1141e304e72e1d0543babe16 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
[please circulate this to any likely candidates - thanks, = Peter]

Research Associate/Senior Research Associate in Applied Seman= tics for Production Architectures

University of Cambridge Computer L= aboratory
Research Associate =C2=A329,301 - =C2=A338,183 or Senior Resea= rch 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/=


Do you want to help build mathematically rigorous foundations f= or real-world computing, to make it more robust and secure?

We have = an ongoing project to establish rigorous semantic models for production mul= tiprocessors, to provide a clear basis for programming, software verificati= on, 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 fo= rm usable for verification. This will provide the first strongly validated = public model for a production multiprocessor architecture. We also have a c= lose collaboration with the CHERI research project, developing processors w= ith hardware-accelerated in-process memory protection and sandboxing, toget= her 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-armv= 8/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 availabl= e to work on:

- the development of our Sail metalanguage for ISA des= cription: a language with a lightweight dependent type system, designed to = capture ARM, IBM POWER, and CHERI instruction semantics in an engineer-frie= ndly way;
- translation from Sail to generate efficient emulators and us= able theorem-prover definitions;
- mechanised proof about the architectu= re definitions, e.g. of security properties, relationships between concurre= ncy models, and correctness results for high-level language concurrency com= pilation; and/or
- development of reasoning, symbolic execution, debuggi= ng, and/or model-checking tools above the architecture definitions - the in= itial work should generate many opportunities along these lines.

The= successful candidate must have a PhD (or equivalent experience), a track-r= ecord of publication in relevant areas of Computer Science, good knowledge = of English and communication skills, and the expertise and commitment to ap= ply rigorous semantics to real systems. We're looking for people with t= he skills to make solid models and tools, well-engineered and widely usable= . You should have expertise in one or more of:

- functional programm= ing (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 con= tribute substantially to future grant applications, it may be possible to a= ppoint at the Senior Research Associate level.

This is part of the b= roader REMS (Rigorous Engineering for Mainstream Systems) programme grant: = a lively collaboration between systems and semantics researchers in Cambrid= ge, Imperial, and Edinburgh to scale up and apply mathematically rigorous s= emantics to mainstream systems.

Informal enquiries should be directe= d to Peter Sewell (Peter.Sewel= l@cl.cam.ac.uk).

To apply online for this vacancy, please click = on the 'Apply' button below. This will route you to the University&= #39;s Web Recruitment System, where you will need to register an account (i= f you have not already) and log in before completing the online application= form.

Please ensure you upload your Curriculum Vitae (CV) and a cov= er letter explaining your potential contribution to the project, as pdf doc= uments. Include the names of 2 or 3 referees at the appropriate point in th= e online application. Your referees should be prepared to send references w= ithin 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 abl= e to consider these as part of your application.

Please quote refere= nce NR10978 on your application and in any correspondence about this vacanc= y.

The University values diversity and is committed to equality of o= pportunity.

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

--001a1141e304e72e1d0543babe16--