[TYPES/announce] Postdoc in Semantics and Tools for Functional Quantum Programming Languages

[Mislove, Michael W]

Dear All,
Below is an announcement for a postdoctoral position working on the MURI project on Semantics and Tools for Functional Quantum Programming Languages. I invite applications from interested candidates.
   Thanks,
   Mike Mislove

===============================================
Michael Mislove                    Phone: +1 504 865-5803<tel:%2B1%20504%20865-5803>
Professor and Chair             FAX:     +1 504 865-5063<tel:%2B1%20504%20865-5063>
Department of Computer Science
Tulane University               URL: http://www.cs.tulane.edu/~mwm
New Orleans, LA 70118 USA
===============================================


Postdoctoral Researcher in Semantics and Tools for Quantum Programming Languages


Applications are invited for a postdoctoral position beginning July 1 and running through November 30, 2018. There is a possibility of an extension beyond November, 2018, depending on funding. The position is in the Department of Computer Science at Tulane University, and will be under the supervision of Professor Michael Mislove.


The successful applicant will work on a project entitled "Semantics, Formal Reasoning, and Tool Support for Quantum Programming”. The project involves designing high-level semantic models and tools to support quantum functional programming languages. A prototype language is Proto-Quipper, which has been  under development (http://www.mathstat.dal.ca/~selinger/quipper/ ). This language uses the circuit model for quantum computation, and envisions languages that support quantum computation under classical control. The overall aim is to design type-safe functional programming languages for quantum computing. The project also involves developing the meta-theory (including categorical semantics) of such languages, and eventually to formalize some of the meta-theory in a proof assistant. The focus of the Tulane work is modeling recursion in such languages, which requires developing quantum domain theory, but interactions with other aspects of the project are expected.


Familiarity with programming language design, and / or semantics is a prerequisite of the position. The latter includes categorical semantics and domain theory. A good knowledge of category theory is also a prerequisite. Of course, familiarity with quantum computing is helpful. Additional components of the project will address issues around quantum information such as non-locality and contextuality,

adapting proof assistants (Coq, Agda, Lean, etc) to develop automated verification for quantum programming languages, and developing quantum routers.


Although the position is at Tulane University, candidates may travel to the other sites where work on this project is taking place. These include UPenn, UIowa and Stanford in the US, as well as McGill University and Dalhousie University in Canada and Oxford and Edinburgh

in the UK.


To apply for this position, direct your browser to the link: https://apply.interfolio.com/41053

Funding for the project comes from the DOD and the U.S. Air Force Office of Scientific Research.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20170314/0aa32a94/attachment-0001.html>