PV2 ⊧ ReVerC, pronounced as "reverse"transforms irreversible programs into reversible circuits

Reversible circuit compiler that has been formally verified in F*. It compiles circuits that operate correctly with respect to the input program.

Application domain/field

• Reversible circuits
• Compilation
• Quantum computing

Type of tool

Compiler

Expected input

Program

Format:

Revs language

Expected output

Combinational reversible circuits with as few ancillary bits as possible which provably cleans temporary values.

Internals

This work focuses on helping a programmer translate classical irreversible programs into a form which a quantum computer can execute. These are called reversible circuits. ReVerC is fully verified, meaning that the circuit compiled by ReVerC will produce the same output for every input as the original source program. ReVerC also provides an assertion checker to verify the source program.

Comments

License: MIT