Software demo: ReVer

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.01635Non UBCUnreviewedAuthor affiliation: University of WaterlooGraduat