A functional language for describing reversible logic

Reversible logic is a computational model where all gates are logically reversible and combined in circuits such that no values are lost or duplicated. This paper presents a novel functional language that is designed to describe only reversible logic circuits. The language includes high-level constructs such as conditionals and a let-in statement that can be used to locally change wires that are otherwise considered to be constant. Termination of recursion is restricted by size-change termination; it must be guaranteed that all recursive calls will be to a strictly smaller circuit size. Reversibility of descriptions is guaranteed with a type system based on linear types. The language is applied to three examples of reversible computations (ALU, linear cosine transformation, and binary adder). The paper also outlines a design flow that ensures garbage-free translation to reversible logic circuits. The flow relies on a reversible combinator language as an intermediate language.