[TYPES/announce] Open postdoc position: "Specification and Verification of Quantum Programming Languages" at CEA and Uni. Paris Sud, France

[Valentin PERRELLE]

The Software Security Lab (LSL, CEA), and the Laboratoire de Recherche 
en Informatique (LRI, University of Paris-Sud) have an open postdoc 
position on the specification and verification of (high-level) quantum 
programs.

The general idea is to explore how the specification/verification 
machinery that has been defined over the years over standard programs 
can be adapted for quantum programs.

If you are interested, please contact Benoît Valiron 
(benoit.valiron at lri.fr), Sébastien bardin (sebastien.bardin at cea.fr) and 
Valentin Perrelle (valentin.perrelle at cea.fr).



------

CEA and University of Paris-Sud
Location: Paris-Saclay, France
Length: 2 years
Keywords: quantum programming, software verification, specification


The Software Security Lab (LSL, CEA), and the Laboratoire de Recherche 
en Informatique (LRI, University of Paris-Sud) have an open postdoc 
position in an area at the intersection of quantum programming and 
software verification, to begin as soon as possible at Paris-Saclay, France.


Context and summary

With the recent interest in the use of quantum algorithms for solving 
concrete problems,  several high-level quantum programming languages 
(QPL) have been designed, in order to fill the gap between quantum 
algorithms and (future) quantum hardware -- for example the Quipper 
language co-developed by Benoît Valiron at LRI. They currently give the 
possibility to implement and analyze real use-cases: emulation, resource 
estimation, etc. Yet, quantum programing is tricky and such quantum 
programs are difficult to write and get right.  There is a clear need 
for dedicated specification and verification mechanisms, allowing to 
express what a quantum program is supposed to do, and then to check it 
more or less automatically. The purpose of this postdoc is precisely to 
design a set of specification and verification tools and techniques for 
high-level quantum programming languages.

A natural starting point will be to study how classical formal methods, 
such as contracts, deductive verification or static analysis, can be 
lifted to QPL. Especially, a first milestone will be to identify a set 
of desirable generic properties over QPL. From an implementation and 
experimentation point of view, the candidate can focus on the 
programming language Quipper and the platform for deductive program 
verification Why3. By designing a formal model of Quipper’s operational 
semantics in Why3, the objective could be to recode Quipper (or a 
suitable subset of it) as embedded language in Why3 and build on the 
model to assert and prove properties of programs.


Tasks

1. Literature review, especially on QPL and classical verification;
2. Specification: understand the kind of desirable properties, how they 
relate or not to classical properties and propose a specification 
language for QPL;
3. Verification: explore how classical verification techniques (to be 
chosen among types, abstract interpretation, deductive verification) 
could be lifted to QPL;
4. Integrate a proof of concept for Quipper.


Host Institutions

LRI is the computer science lab of Universite Paris Sud. Founded more 
than 35 years ago, it has over 240 members, including 110 faculty and 
staff and 90 Ph.D. students. LRI consists of eight research groups 
covering a wide spectrum of subjects ranging from fundamental to applied 
research. The tool Why3 was founded at LRI, and is still actively 
developed within the team VALS. Quantum computation is one of the topics 
covered by the teams Parsys and Modhel. Parsys is considering it for its 
relation to HPC while Modhel works on quantum programming languages and 
their semantics, including the Quipper language.

Within CEA LIST, LSL is a twenty-person team dedicated to software 
verification, with a strong focus on real-world applicability and 
industrial transfer. LSL designs methods and tools that leverage 
innovative approaches to ensure that real-world systems can comply with 
the highest safety and security standards. Especially, the team develops 
and maintains the open-source Frama-C platform for C code verification.
Both CEA LIST and LRI are located at the heart of Campus Paris Saclay, 
in the largest European cluster of public and private research.


Application

Candidates should have a Ph.D. in Computer Science, or be near completion.

We are mainly looking for candidates with a strong background in 
Software Verification interested in exploring Quantum Programing but we 
are also interested by candidates from Quantum Computation who wants to 
explore Formal Verification.

Applicants should send an email to Benoït Valiron 
(benoit.valiron at lri.fr),   Sébastien Bardin (sebastien.bardin at cea.fr) 
and Valentin Perrelle (valentin.perrelle at cea.fr) including CV, 
motivation letter and  reference.




-------------- next part --------------
A non-text attachment was scrubbed...
Name: postdoc-quantum.pdf
Type: application/pdf
Size: 151414 bytes
Desc: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20171009/4b50a2a1/attachment-0001.pdf>