< Retour au sommaire

Qbrick, a core development framework for certified quantum programming

Christophe Charreton le

Lieu: salle 1073, bât 862

Due to the nature of quantum computation, we believe that, in this field, formal verification is meant to play a role similar to that of test development in classical computing. In this talk we present Qbricks, a core programming language for entirely verifiable quantum programming, embedded into Why3. Qbricks both provides programming functions such as in other programming languages and formal analysis means enabling to specify and verify the written programs. We believe this two layers approach is necessary for widespread verified programming methodology. We present our implementation of both the matrix and the path-sum semantics for quantum processes and the first fully verified equivalence proof between those. In addition, we implemented various further semantics artifacts for quantum circuits semantics. Thanks to Qbricks, we present a verified implementation of the phase estimation algorithm (roughly, the quantum part of the famous Shor algorithm). This is, as far as we know, the first scale-invariant proof of a non-trivial quantum routine.

Download slides