Postdoctoral Position

Postdoctoral Position

[Mislove, Michael W]

[-- Attachment #1: Type: text/plain, Size: 108 bytes --]

[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


[-- Attachment #2.1.1: Type: text/plain, Size: 2785 bytes --]

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. 

[-- Attachment #2.1.2: Type: text/html, Size: 7192 bytes --]

[-- Attachment #2.2: smime.p7s --]
[-- Type: application/pkcs7-signature, Size: 1579 bytes --]