1 Department of Computer Science, Faculty of Science, Københavns Universitet2 Administration, Department of Computer Science, Faculty of Science, Københavns Universitet3 Administration, Department of Computer Science, Faculty of Science, Københavns Universitet
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.
Proceedings of the 2012 Forum on Specification and Design Languages, 2012, p. 135-142
Main Research Area:
2012 Forum on specification & Design Languages, 2012