[TYPES/announce] Postdoc position in quantum formal verification @ Université Paris-Saclay, CEA List, France

[christophe chareton]

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... at 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 at cea.fr, sebastien.bardin at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20211201/fb13a053/attachment-0001.htm>