Matthew Amy, PhD candidate
David R. Cheriton School of Computer Science
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 where estimation of the resources required to implement an algorithm factors heavily in the guidance of security policies.
In this seminar I will describe the design and formal verification of a reversible circuit compiler, ReVerC. The compiler compiles a classical, irreversible language Revs to combinational reversible circuits, optimizing for space-usage along the way. The formal verification of ReVerC was carried out in F*, a lightweight dependently typed language, which combined with a partial evaluation-based structure allowed for rapid verification approaching a 1:1 code to proof ratio.
Joint work with Martin Roetteler and Krysta Svore.