PhD student in formal semantics and verification for quantum computing

Information about the project
This project is part of QuantumStack, a 5-year project funded by the Swedish Foundation for Strategic Research, with the aim of developing a full software stack for programming quantum computers. The project is integrated with the Wallenberg Centre for Quantum Technology (WACQT), a 12-year, billion-SEK initiative started in 2018 with the purpose of advancing Swedish academia and industry to the forefront of quantum technology, and to build a Swedish quantum computer. Our ambitious goal at Chalmers is to build this quantum computer with 100 superconducting qubits and to apply it to real computational problems that cannot be efficiently solved on a conventional computer. Such computationally hard problems are found, e.g., in optimization, quantum chemistry, materials science, machine learning, etc.

So far there has been a separation between the theory of quantum computing as studied by Computer Scientists and mathematicians, and the work that physicists have been doing on the quantum computers that exist today. We want to create a compilation stack that will bridge this gap, and we want to use the techniques of type theory and formal logic to ensure that the stack is sound.

We are now seeking a PhD student to create formal semantics for the languages involved in the compilation stack, develop tools for verifying that each stage in the compilation stack is sound, and develop domain-specific languages (DSLs) for the stages of the compilation stack including the control pulses that are fed to the qubits.

This work is both important practically, and a fascinating theoretical challenge - to find the correct logic(s) and type theory for describing and reasoning about quantum algorithms - which may itself give insight into the physical universe. You will also have the opportunity to see the results applied to real quantum computers as the project proceeds.

This project is funded by SSF (https://strategiska.se/en/) under their call for "Future Software Systems".

The division of Computing Science pursues research and education that advances the design of secure and trustworthy software and systems, from theoretical foundations, and up through the design and implementation of programming languages and tools. The focus of the Logic and Types group within the division is on dependent type theory, and is best known for the development of well-known proof assistants, including the Agda system.

Major responsibilities
The main responsibilities of a PhD student at Chalmers consist in pursuing doctoral studies by conducting research within your project, in collaboration and independently, leading to results that you will publish in journals and present at meeting and conferences.

Your studies also include coursework in your field and common core courses on generic and transferable skills. The position generally also includes teaching on the undergraduate level or other duties corresponding to up to 20 per cent of working hours.

Qualifications
Required qualifications:
*MSc in Computer Science, Mathematics, Physics, or equivalent
*Excellent communication skills in written and spoken English

Desired qualifications: One or more of
* Ability to program in functional languages such as Haskell or ML
* Experience with quantum computing
* Experience with type theory
* Experience with proof assistants such as Coq or Agda

We value a collaborative attitude and an interest in working both in teams and independently. Self-motivation, attention to detail, and a problem-solving analytical ability are important personal qualities for this position.

Contract terms
Full-time temporary employment. The position is limited to a maximum of five years.

We offer
Chalmers offers a cultivating and inspiring working environment in the coastal city of Gothenburg. 
Read more about working at Chalmers and our benefits for employees. Chalmers offers Swedish courses.

Chalmers aims to actively improve our gender balance. We work broadly with equality projects, for example the GENIE Initiative on gender equality for excellence. Equality and diversity are substantial foundations in all activities at Chalmers.

Application procedure
Read more and apply here.

Application deadline: 31st August, 2022

For questions, please contact: 
Associate Professor Robin Adams, Computing Science at CSE
E-mail: robinad@chalmers.se, +46 31-772 6348

*** Chalmers declines to consider all offers of further announcement publishing or other types of support for the recruiting process in connection with this position. ***