type theory postdoc at Dalhousie University
Peter Selinger <selinger <at> mathstat.dal.ca>
2015-10-01 01:20:27 GMT
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.