[TYPES/announce] Postdoc in SDN verification and security at Edinburgh

[David Aspinall]

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear All,

We have an opening for a postdoctoral Research Associate to work on
formal modelling and verification for network security applications of
SDN (Software Defined Networking) at University of Edinburgh.

For details please see here:

https://www.vacancies.ed.ac.uk/pls/corehrrecruit/erq_jobspec_version_4.jobspec?p_id=038513

The post is available for a year with a possibility of extension subject
to funding.  It would suit somebody with a background in (ideally)
formal methods, networking and security.

I welcome people to contact me to discuss informally.

 - David

--
Prof. David Aspinall, Email: david.aspin...@ed.ac.uk
LFCS, School of Informatics,  URL: http://homepages.inf.ed.ac.uk/da
University of Edinburgh,  Office: +44 (0)131 650 5177
10 Crichton Street,   Mobile: +44 (0)773 809 2693
Edinburgh.  EH8 9AB   U.K.Office:  Room 5.12A, Inf. Forum

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Re: [TYPES/announce] Postdoc position in Applied Semantics for Production Architectures

[Peter Sewell]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

On 15 December 2016 at 23:20, 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 £29,301 - £38,183 or Senior Research Associate £39,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.sew...@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 

[TYPES/announce] Call for papers: QPL 2017

[Aleks Kissinger]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

   CALL FOR PAPERS

 The 14th International Conference on
  Quantum Physics and Logic (QPL)

July 3-7, 2017
  Radboud Universiteit, Nijmegen, Netherlands

  http://qpl.cs.ru.nl


The 14th International Conference on Quantum Physics and Logic (QPL)
will take place at Radboud University between Monday 3 and
Friday 7 July, 2017.

The conference brings together researchers working on mathematical
foundations of quantum physics, quantum computing, and related areas,
with a focus on structural perspectives and the use of logical tools,
ordered algebraic and category-theoretic structures, formal languages,
semantical methods, and other computer science techniques applied to
the study of physical behaviour in general. Work that applies
structures and methods inspired by quantum theory to other fields
(including computer science) is also welcome.

Previous QPL events were held in Glasgow (2016), Oxford (2015),
Kyoto (2014), Barcelona (2013), Brussels (2012), Nijmegen (2011),
Oxford (2010), Oxford (2009), Reykjavik (2008), Oxford (2006),
Chicago (2005), Turku (2004), and Ottawa (2003).


INVITED SPEAKERS

Jamie Vicary
Miguel Navasques
Matthias Christandl
Paulo Perinotti


INVITED TUTORIALS

Bart Jacobs (effectus theory)
Dan Marsden (categorical string diagrams)
Ronald de Wolf (quantum algorithms)
Simon Perdrix (TBC)


SATELLITES

There will be a satellite workshop on Quantum Structures hosted by
the International Quantum Structures Association (IQSA) from
Tuesday July 4th to Friday the 7th. Look out for details on the
QPL website and via an official announcement later this year!


IMPORTANT DATES

Submission: 21 April, 2017
Notification: 29 May
Papers ready: 23 June
Conference: 3-7 July



SUBMISSIONS

Prospective speakers are invited to submit a contribution to the
conference.

 - Original contributions consist of a 5-12 page extended abstract
   which provides sufficient evidence of results of genuine interest
   and enough detail to allow the program committee to assess the
   merits of the work. Submission of substantial albeit partial
   results of work in progress is encouraged. Authors of accepted
   papers will be invited to give long or short talks, depending on
   the quality and/or maturity of the submission.

 - Extended abstracts describing work submitted/published elsewhere
   will also be considered, provided the work is recent and relevant
   to the conference. These consist of a 3 page description and should
   include a link to a separate published paper or preprint.


Extended versions of accepted original research contributions will be
published in Electronic Proceedings in Theoretical Computer Science
(EPTCS) after the conference.

Submissions should be prepared using LaTeX, and must be submitted
in PDF format. Use of the EPTCS style is encouraged. Submission is
done via EasyChair:

https://www.easychair.org/conferences/?conf=qpl2017

There will be an award for the best paper whose authors are all
students, at the discretion of the programme committee.


REGISTRATION

Registration will be opened later, please visit the website for more
details.


PROGRAMME COMMITTEE

Aleks Kissinger (Radboud, co-chair)
Bob Coecke (Oxford, co-chair)
Bart Jacobs (Radboud)
Benoit Valiron (Paris-Sud)
Benno Van Den Berg (Amsterdam)
Chris Heunen (Edinburgh)
Dan Browne (University College London)
Daniel Oi (Strathclyde)
Dominic Horsman (Durham)
Dusko Pavlovic (Hawaii)
Giulio Chiribella (Hong Kong)
Hans Maassen (Radboud)
Isar Stubbe (Littoral-Cote-d'Opale)
Jamie Vicary (Oxford)
Joachim Kock (Barcelona)
John Baez (UC Riverside)
Kohei Kishida (Oxford)
Matt Leifer (Chapman)
Matty Hoban (Oxford)
Michael Moortgat (Utrecht)
Mingsheng Ying (UT Sydney)
Miriam Backens (Bristol)
Paolo Perinotti (Pavia)
Paul-Andre Mellies (Paris Diderot)
Pawel Sobocinski (Southampton)
Peter Selinger (Dalhousie)
Prakash Panangaden (McGill)
Rick Blute (Ottowa)
Rob Spekkens (Permiter Institute)
Robert Raussendorf (British Columbia)
Ross Duncan (Strathclyde)
Samson Abramsky (Oxford)
Simon Gay (Glasgow)
Simon Perdrix (CNRS Nancy)


STEERING COMMITTEE

Bob Coecke (University of Oxford)
Prakash Panangaden (McGill University)
Peter Selinger (Dalhousie University)


LOCAL ORGANISATION

Aleks Kissinger
Bart Jacobs
Sander Uijlen

[TYPES/announce] MFPS 33: first call for papers

[Alexandra Silva]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


The 33rd Conference on the Mathematical Foundations of Programming Semantics 
(MFPS XXXIII) 
will take place on the campus of Ljubljana University, Slovenia, between 12 and 
15 June 2017. MFPS conferences are dedicated to the areas of mathematics, 
logic, and computer 
science that are related to models of computation in general, and to semantics 
of programming 
languages in particular. This is a forum where researchers in mathematics and 
computer science 
can meet and exchange ideas. The participation of researchers in neighbouring 
areas is strongly
encouraged.

Topics include, but are not limited to, the following:
bio-computation; concurrent qualitative and quantitative distributed
systems; process calculi; probabilistic systems; constructive
mathematics; domain theory and categorical models; formal languages;
formal methods; game semantics; lambda calculus; programming-language
theory; quantum computation; security; topological models; logic; type
systems; type theory. We also welcome contributions that address
applications of semantics to novel areas such as complex systems,
markets, and networks, for example.

Conference home page: http://coalg.org/mfps-calco2017

## INVITED SPEAKERS

*  Rehana Patel, Olin College 
*  Laura Kovacs, TU Wien 
*  Dexter Kozen, Cornell University 
*  Amr Sabry, Indiana University 

## TUTORIAL SPEAKERS AND SPECIAL SESSIONS

*  Laure Daviaud, Warsaw 
  - Algebraic automata theory

*  Nate Foster, Cornell 
  - Foundations of Network Programming, special session in honour of Dexter 
Kozen’s 65th Birthday

*  Ben Worrell, Oxford
  - Metrics and Privacy (Joint MPFS & CALCO)

*  Derek Dreyer, MPI-SWS
  - Formal Verification

## SUBMISSION

### Important dates:

* Submission Deadline: March 10 
* Notification: April 28
* Proceedings: May 19 
* Conference: June 12-15


### Submitting

Submissions should be prepared using the [ENTCS
Macros](http://www.entcs.org/), in the form of a PDF file not
exceeding 15 pages. Submissions are open on
[EasyChair] (https://easychair.org/conferences/?conf=mfps33).

### Proceedings

A preliminary version will be distributed at the meeting. Final
proceedings will appear in ENTCS after the meeting.

## PROGRAM COMMITTEE:

Gilles Barthe, Madrid, Spain
Andrej Bauer, Ljubljana, Slovenia
Steve Brookes, Pittsburgh, PA, USA
Carla Ferreira, Lisbon, Portugal
Nate Foster, Ithaca, NY, USA
Chris Heunen, Edinburgh, UK
Justin Hsu, Philadelphia, PA, USA
Achim Jung, Birmingham, UK
Elham Kashefi, Edinburgh, UK
Clemens Kupke, Glasgow, UK
Barbara Koenig, Duisburg, Germany
Catherine Meadows, NRL , USA
Andrzej Murawski, Warwick, UK,
Bart Jacobs, Radboud U, Netherlands
Bob Coecke, Oxford, UK
Cameron Freer, Cambridge MA, USA
Catherine Meadows, Washington, DC, USA
Michael Mislove, New Orleans, LA, USA
Joel Ouaknine, Saarbrucken, Germany
Alessandra Palmigiano, Delft, The Netherlands
Prakash Panangaden, Montreal, Canada
Daniela Petrisan, Paris, France
Brigitte Pientka, Montreal, Canada
Jurriaan Rot, Nijmegen, The Netherlands 
Mehrnoosh Sadrzadeh, London, UK
Alexandra Silva (Chair), London, UK 
Ana Sokolova, Salzburg, Austria 
Valeria Vignudelli, Bologna, Italy 


## LOCAL ORGANISERS:

* Matja Pretnar 
* Andrej Bauer

[TYPES/announce] postdoc position (5 years) in Innsbruck

[Aart Middeldorp]

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

  5 year postdoc position in computational logic
  ==

The University of Innsbruck invites applications for a 5 year postdoctoral
position in the Computational Logic research group. Candidates must hold a
PhD degree in computer science. A strong background in computational logic
(in particular automated and interactive theorem proving, SMT solving, term
rewriting, type theory) is desired. The ideal candidate enjoys working with
students at all levels. Candidates are expected to conduct research leading
to a habilitation and contribute to teaching and administration. Knowledge
of German is not essential.

The position is a full-time "B1/3 position" with teaching obligations of
4 hours per semester. The annual gross salary is approximately EUR 50,000.
The official job advert (reference MIP-9118) appeared at

http://orawww.uibk.ac.at/public/karriereportal.details?asg_id_in=9118

Applications (including CV, publication list, and two letters of
recommendation) must be submitted electronically at

https://orawww.uibk.ac.at/public/karriereportal.bewerben?page=w_id=9118

no later than 2 February 2017. The starting date for the position is
1 March 2017. Informal inquiries may be addressed to

aart.middeldorp at uibk.ac.at

The city of Innsbruck, which hosted the Olympic Winter Games in 1964 and
1976, is superbly located in the beautiful surroundings of the Tyrolean
Alps. The combination of the Alpine environment and urban life in this
historic town provides a high quality of living.

Further information is available from the following links:

Computational Logic:
http://cl-informatik.uibk.ac.at/

Department of Computer Science:
http://informatik.uibk.ac.at/

University of Innsbruck:
http://www.uibk.ac.at/

City of Innsbruck:
http://www.innsbruck.at/