Logic List Mailing Archive

Postdoctoral position (2y) in quantum programming & formal methods, Paris (France), Deadline: early Feb 2022

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 GROUP

We are an emerging group in formal verification and static analysis of 
quantum programs, integrated in the Software Safety Laboratory of CEA 
List, Universite 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.

=== 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.chareton@cea.fr, sebastien.bardin@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.
--
[LOGIC] mailing list
http://www.dvmlg.de/mailingliste.html
Archive: http://www.illc.uva.nl/LogicList/

provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam