36
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Hoare Logic for Quantum Programs

      Preprint

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          Hoare logic is a foundation of axiomatic semantics of classical programs and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.

          Related collections

          Most cited references7

          • Record: found
          • Abstract: not found
          • Article: not found

          Towards a quantum programming language

            Bookmark
            • Record: found
            • Abstract: found
            • Article: found
            Is Open Access

            Toward an architecture for quantum programming

            , , (2003)
            It is becoming increasingly clear that, if a useful device for quantum computation will ever be built, it will be embodied by a classical computing machine with control over a truly quantum subsystem, this apparatus performing a mixture of classical and quantum computation. This paper investigates a possible approach to the problem of programming such machines: a template high level quantum language is presented which complements a generic general purpose classical language with a set of quantum primitives. The underlying scheme involves a run-time environment which calculates the byte-code for the quantum operations and pipes it to a quantum device controller or to a simulator. This language can compactly express existing quantum algorithms and reduce them to sequences of elementary operations; it also easily lends itself to automatic, hardware independent, circuit simplification. A publicly available preliminary implementation of the proposed ideas has been realized using the C++ language.
              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              Quantum Programming

                Bookmark

                Author and article information

                Journal
                24 June 2009
                Article
                0906.4586
                6a89b36c-0953-4801-b0e1-735224046775

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                50 pages
                quant-ph

                Comments

                Comment on this article