From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9059 Path: news.gmane.org!.POSTED!not-for-mail From: selinger@mathstat.dal.ca (Peter Selinger) Newsgroups: gmane.science.mathematics.categories Subject: Two postdoc positions at Dalhousie Date: Thu, 15 Dec 2016 22:06:18 -0400 (AST) Message-ID: Reply-To: selinger@mathstat.dal.ca (Peter Selinger) NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: blaine.gmane.org 1481901747 31086 195.159.176.226 (16 Dec 2016 15:22:27 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Fri, 16 Dec 2016 15:22:27 +0000 (UTC) To: categories@mta.ca (Categories List) Original-X-From: majordomo@mlist.mta.ca Fri Dec 16 16:22:23 2016 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.7.28]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1cHuKy-0006pH-6v for gsmc-categories@m.gmane.org; Fri, 16 Dec 2016 16:22:20 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:52706) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1cHuKH-0005Gc-Lt; Fri, 16 Dec 2016 11:21:37 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1cHuKI-0002zU-Cf for categories-list@mlist.mta.ca; Fri, 16 Dec 2016 11:21:38 -0400 X-Mailer: ELM [version 2.5 PL8] Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9059 Archived-At: Dear colleagues, I invite applications for two postdoctoral position, starting early in 2017 (ideally in January or February), at Dalhousie University under my supervision. The successful applicants will work on a project entitled "Trusted Quantum Software via a Formally Verified Functional Quantum Programming Language". Specifically, the project involves the design and semantics of a functional programming language for quantum computing, loosely modelled on the Quipper language (http://www.mathstat.dal.ca/~selinger/quipper/). It will also involve developing the meta-theory of the language, and eventually the formalization of some of this meta-theory in a proof assistant. The research project is part of a team effort, also involving collaborators from Tulane, Stanford, Oxford, the University of Iowa, and the University of Pennsylvania. Familiarity with type theory, programming language design, and/or semantics (including categorical semantics) will be a prerequisite for these postdocs. Familiarity with quantum computing will be helpful, but is neither necessary nor sufficient for this position - the main emphasis is on programming languages and type systems. The positions are initially for 1 year, and can be extended for an additional year. The salary is $50,000 Canadian per year plus benefits. Two positions are available: * Postdoc 1 is funded by the U.S. Air Force Office of Scientific Research. The postdoc will be held in the Department of Mathematics and Statistics at Dalhousie University. * Postdoc 2 is funded by Rigetti Computing, a quantum computing startup based in Berkeley, California (rigetti.com). The postdoc position is formally known as the "Rigetti Computing Prize Fellowship". The postdoc will be held in the Department of Mathematics and Statistics at Dalhousie University, but the applicant will be expected to spend three months per year on site at Rigetti Computing office in Berkeley to work on Rigetti projects related to quantum computing. Interested applicants should contact Peter Selinger at selinger@mathstat.dal.ca as soon as possible, and in any case before January 10. I can provide more details about the research project to interested applicants on request. Thanks, -- Peter [For admin and other information see: http://www.mta.ca/~cat-dist/ ]