[TYPES/announce] Postdoctoral Position Closing

[Mislove, Michael W]

Dear All,
This is a reminder that the closing date for the postdoctoral position listed below is April 30.
  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

Tulane University is an equal employment opportunity/affirmative action/persons with disabilities/veterans employer committed to excellence through diversity. Tulane will not discriminate against individuals with disabilities or veterans. All eligible candidates are encouraged to apply.

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/20170426/2a8069e6/attachment-0001.html>