Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E

                   ______                __    _               
                  / ____/___ _____ ___  / /_  (_)_  ______ ___ 
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/ 

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                           Lundi 2 décembre, 10h30

                             -------------------
                             Christophe Chareton
                             -------------------

                                 CEA puis LRI

    ======================================================================
    Qbrick, a core development framework for certified quantum programming
    ======================================================================

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. This is, as far as we know, the first scale-invariant proof of a
non-trivial quantum routine.