[ 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.
