BIRS Workshop Lecture Videos

Banff International Research Station Logo

BIRS Workshop Lecture Videos

Software demo: ReVer Amy, Matt


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.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International