[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
The emerging quantum software group @ CEA List, Université Paris-Saclay, offers
2 fully-funded positions at the crossroad of quantum programming, program
analysis and formal methods.
=== OUR GROUP
We are an emerging group in formal verification and static analysis of quantum
programs, integrated in the Software Safety Laboratory of CEA List, Université
Paris-Saclay. Our long term goal is to design and develop formal techniques and
tools enabling productive and certified quantum programming. Especially, we
develop Qbricks [1], a proof of concept environment for formally verified
quantum programming language.
See our website at https://qbricks.github.io/ for additional information.
=== Position#1 (3 years PhD) Probing quantum verification in the NISQ era
The goal of this doctoral position is to probe formal verification against
first generation of quantum application (NISQ era). Possibilities include,
among other: extending Qbricks semantic and proof model to the hybrid paradigm,
develop and implement a specification and proof system for error propagation
and correction in quantum computing, develop certified ready-to-use NISQ
applications.
Keywords: quantum programming, formal verification, NISQ, quantum error
correction
=== Position#2 (2 years PostDoc)
The goal of this post-doctoral position is to extend formal verification
practice to quantum compilation. Possibilities include, among others, error
correction mechanisms in certified quantum code, together with specifications
and reasoning technique for certifying its reliability, automatized certified
optimizer for quantum circuits, hardware agnostic assembly language together
with its compiler,
Keywords: quantum programming, compilation, optimization, formal verification
=== HOW TO APPLY
Applications should be sent to [email protected] as soon as possible
(first come, first served) and by early July 2021 at the latest. Candidates
should send a CV, a cover letter, a transcript of all their university results,
as well as contact information of two references. Each position is expected to
start in October 2021.
Advisors: Sébastien Bardin (CEA), Christophe Chareton (CEA)
Contact: [email protected]
[1] C. Chareton, S. Bardin, F. Bobot, V. Perrelle, and B. Valiron. An Automated
Deductive Verification Framework for Circuit-building Quantum Programs. ESOP
2021.
