Verified compilation of space-efficient reversible circuits
From MaRDI portal
Quantum algorithms and complexity in the theory of computing (68Q12) Theory of compilers and interpreters (68N20) Other nonclassical models of computation (68Q09) Specification and verification (program logics, model checking, etc.) (68Q60) Networks and circuits as models of computation; circuit complexity (68Q06)
Abstract: The generation of reversible circuits from high-level code is an important problem in several application domains, including low-power electronics and quantum computing. Existing tools compile and optimize reversible circuits for various metrics, such as the overall circuit size or the total amount of space required to implement a given function reversibly. However, little effort has been spent on verifying the correctness of the results, an issue of particular importance in quantum computing. There, compilation allows not only mapping to hardware, but also the estimation of resources required to implement a given quantum algorithm, a process that is crucial for identifying which algorithms will outperform their classical counterparts. We present a reversible circuit compiler called ReVerC, which has been formally verified in F* and compiles circuits that operate correctly with respect to the input program. Our compiler compiles the Revs language to combinational reversible circuits with as few ancillary bits as possible, and provably cleans temporary values.
Recommendations
Cited in
(13)- \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
- Towards large-scale functional verification of universal quantum circuits
- A framework for quantum-classical cryptographic translation
- \textit{Re}\(\mathcal{Q}\)\textsc{wire}: reasoning about reversible quantum circuits
- Uncomputation in the Qrisp high-level quantum programming framework
- An automated deductive verification framework for circuit-building quantum programs
- Estimating the cost of generic quantum pre-image attacks on SHA-2 and SHA-3
- Tools for quantum and reversible circuit compilation
- Generating reversible circuits from higher-order functional programs
- Sized Types for Low-Level Quantum Metaprogramming
- Compact Realization of Reversible Turing Machines by 2-State Reversible Logic Elements
- REVS: a tool for space-optimized reversible circuit synthesis
- Reversible simulation of space-bounded computations
This page was built for publication: Verified compilation of space-efficient reversible circuits
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2164204)
