Applications are invited for a postdoctoral position beginning January 2019 and running through November 30, 2020. The successful applicant will work on a project entitled "Semantics, Formal Reasoning, and Tool Support for Quantum Programming.” The project involves designing semantic models and tools to support high-level quantum functional programming languages. A prototype is Proto-Quipper (http://www.mathstat.dal.ca/~selinger/quipper/ ). Proto-Quipper and its dialects use the circuit model for quantum computation that follows the “quantum computation under classical control” paradigm. The goal 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 formalizing some of the meta-theory in a proof assistant. So far, attention has been confined to circuit description languages that include a linear sublanguage to model quantum circuits. The focus of the Tulane work has been to add recursion to the models of these languages. Our work has focused on the linear/nonlinear models first devised by Benton for linear logic, from which we have extracted the ingredients needed to model circuit description languages. Progress along this line includes a model for term recursion, with a model supporting recursive intuitionistic types nearing completion.

The next goals include adding dynamic lifting, which would allow support for quantum computation, rather than being confined to describing circuits. We are also interested in developing concrete models based on C*- and W*-algebras, and operator systems, more generally. Problems in contextuality as a resource for demonstrating quantum advantage also are of interest.

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

Funding for the project comes from the DOD and the U.S. Air Force Office of Scientific Research.

Minimum qualifications:

• Knowledge of quantum computation and quantum information.
• Knowledge of category theory.
• PhD in computer science or a related area.

Preferred Qualifications:

• Knowledge of programming language design, type theory, and semantic models.
• Familiarity with Hilbert space formalism and/or categorical quantum mechanics.
• Familiarity with proof assistants such as Coq, Agda or LEAN.
• Record of peer-reviewed publications at conferences or in journals.

Candidates must apply via Interfolio and provide the following:

• CV
• Cover letter
• Three letters of recommendation for the project
• A statement describing previous research work, as well as research problems that interest the applicant

To receive full consideration, applications should be received by December 1st.