From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8710 Path: news.gmane.org!not-for-mail From: selinger@mathstat.dal.ca (Peter Selinger) Newsgroups: gmane.science.mathematics.categories Subject: type theory postdoc at Dalhousie University Date: Wed, 30 Sep 2015 22:20:27 -0300 (ADT) Message-ID: Reply-To: selinger@mathstat.dal.ca (Peter Selinger) NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1443707033 27327 80.91.229.3 (1 Oct 2015 13:43:53 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Thu, 1 Oct 2015 13:43:53 +0000 (UTC) To: categories@mta.ca (Categories List) Original-X-From: majordomo@mlist.mta.ca Thu Oct 01 15:43:40 2015 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.7.22]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Zhe90-0003VV-Re for gsmc-categories@m.gmane.org; Thu, 01 Oct 2015 15:43:35 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:58945) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1Zhe7v-0005BJ-0x; Thu, 01 Oct 2015 10:42:27 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1Zhe7v-0001MG-BA for categories-list@mlist.mta.ca; Thu, 01 Oct 2015 10:42:27 -0300 X-Mailer: ELM [version 2.5 PL8] Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8710 Archived-At: Dear colleagues, I invite applications for one postdoctoral position, starting between now and January 1, at Dalhousie University under my supervision. The successful applicant will work on a project entitled "Trusted Quantum Software via a Formally Verified Functional Quantum Programming Language". Specifically, the project will involve the design of a type system for a type-safe 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 (including categorical semantics) of the language, and eventually the formalization of some of this meta-theory in a proof assistant. Familiarity with type theory (especially dependent type theory), programming language design, and/or semantics will be a prerequisite for this postdoc. 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. Although the position will be held at Dalhousie University in Canada, it will be an asset if the candidate is able to travel, because I will be spending one semester in Germany and one semester in the U.S. next year, and ideally I would like the postdoc to be able to accompany me. Funding for the project comes from the U.S. Air Force Office of Scientific Research, and the research project will be part of a team effort also involving collaborators from Tulane, Stanford, Oxford, the University of Iowa, and the University of Pennsylvania. The nominal start date for the project is September 30, 2015 (yes, this is today!), so the start date can be immediately, or some time in the near future. The position is initially for 1 year, and can be extended for an additional year. The salary is CAD $60,000 per year. Interested applicants should contact Peter Selinger at selinger@mathstat.dal.ca as soon as possible, and in any case before October 21. 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/ ]