[TYPES/announce] Postdoctoral Position

[Mislove, Michael W]

Dear All,
Below is an announcement of a postdoctoral research position starting October 1 and running through November 30, 2018. I encourage all interested parties to apply. 
   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 <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 October 1, 2017 and running through November 30, 2018. 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/ <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. 

To apply for one of this position, direct your browser to the link: https://apply.interfolio.com/41053 <http://apply.interfolio.com/33550>

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/20170726/50a218f7/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 1579 bytes
Desc: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20170726/50a218f7/attachment-0001.p7s>