[TYPES/announce] postdoc position in dependent types at Dalhousie

[Peter Selinger]

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 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 at 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