Theses and Dissertations from UMD

Permanent URI for this communityhttp://hdl.handle.net/1903/2

New submissions to the thesis/dissertation collections are added automatically as they are received from the Graduate School. Currently, the Graduate School deposits all theses and dissertations from a given semester after the official graduation date. This means that there may be up to a 4 month delay in the appearance of a give thesis/dissertation in DRUM

More information is available at Theses and Dissertations at University of Maryland Libraries.

Browse

Filters

20221

Settings

Author: search.filters.author.Hietala, KeshaSubject: search.filters.subject.Compilers

Search Results

Now showing 1 - 1 of 1
  • Thumbnail Image
    Item
    A Verified Software Toolchain for Quantum Programming
    (2022) Hietala, Kesha; Hicks, Michael; Computer Science; Digital Repository at the University of Maryland; University of Maryland (College Park, Md.)
    Quantum computing is steadily moving from theory into practice, with small-scale quantum computers available for public use. Now quantum programmers are faced with a classical problem: How can they be sure that their code does what they intend it to do? I aim to show that techniques for classical program verification can be adapted to the quantum setting, allowing for the development of high-assurance quantum software, without sacrificing performance or programmability. In support of this thesis, I present several results in the application of formal methods to the domain of quantum programming, aiming to provide a high-assurance software toolchain for quantum programming. I begin by presenting SQIR, a small quantum intermediate representation deeply embedded in the Coq proof assistant, which has been used to implement and prove correct quantum algorithms such as Grover’s search and Shor’s factorization algorithm. Next, I present VOQC, a verified optimizer for quantum circuits that contains state-of-the-art SQIR program optimizations with performance on par with unverified tools. I additionally discuss VQO, a framework for specifying and verifying oracle programs, which can then be optimized with VOQC. Finally, I present exploratory work on providing high assurance for a high-level industry quantum programming language, Q#, in the F* proof assistant.