Open Collections

Software demo: ReVer

Banff International Research Station for Mathematical Innovation and Discovery

A variety of tools exist which can compile classical, irreversible code into reversible circuits. However, little effort has been spent on verifying these tools, potentially allowing compiler errors to cause incorrect results and negatively affect resource estimation. In this talk I will describe the design and implementation of a formally verified, optimizing reversible circuit compiler. Our compiler, called ReVer, compiles the simple ML-like language Revs to reversible circuits, with optimizations to reduce the number of ancilla bits used. We use the dependently typed language F* to verify with machine-checked proofs that ReVer compiles circuits that operate correctly with respect to the input program and cleans all temporary bits. Joint work with Martin Roetteler and Krysta Svore. http://arxiv.org/abs/1603.01635

Mathematics; Quantum theory; Information and communication, circuits; Theoretical computer science

video/mp4

Author affiliation: University of Waterloo

2016-10-19

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/59505

Unreviewed

http://creativecommons.org/licenses/by-nc-nd/4.0/