[ 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 a two years fully-funded postdoctoral position 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://urldefense.com/v3/__https://qbricks.github.io/__;!!IBzWLUs!DTmRMuyfh6ehH9DSFJaqLMIs4YlesQRyI8Q8dkpjvQlB5Tx-NTs4Fg265PDuyMEj-jAvzHF-RqvC7g$ for additional information. === ABOUT THE POSTDOC POSITION Adapting the best practice for classical computing formal verification -- deductive verification, first order logic reasoning--, our recent development of Qbricks enables formal specification -- circuit well-formedness, functional behavior, complexity -- 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 === HOW TO APPLY Applications should be sent to christophe.char...@cea.fr as soon as possible (first come, first served) and by early February 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. The position is expected to start in May 2021. Advisors: Christophe Chareton (CEA), Sébastien Bardin (CEA) Contact: christophe.chare...@cea.fr, sebastien.bar...@cea.fr [1] C. Chareton, S. Bardin, F. Bobot, V. Perrelle, and B. Valiron. An Automated Deductive Verification Framework for Circuit-building Quantum Programs. ESOP 2021.