Postdoctoral position (2y) in quantum programming & formal methods, Paris (France)

The emerging quantum software group @ CEA List, Universite Paris-Saclay, offers a two years fully-funded postdoctoral position at the crossroad of quantum programming, program analysis and formal methods.

Our long term goal is to design and develop formal techniques and tools enabling productive and certified quantum programming. Especially, we develop Qbricks, a proof of concept environment for formally verified quantum programming language. Adapting the best practice for classical computing formal verification, our recent development of Qbricks enables formal specification and verification for quantum programming with ideal qubits. The goal of this post-doctoral position is to extend this practice to quantum compilation and physical qubits implementations. 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, qubit mapping, etc.

Keywords: quantum programming, compilation, optimization, formal verification, deductive verification.