A functional language for describing reversible logic

TY - GEN

T1 - A functional language for describing reversible logic

AU - Thomsen, Michael Kirkedal

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

M3 - Article in proceedings

SN - 978-1-4673-1240-0

SP - 135

EP - 142

BT - Proceedings of the 2012 Forum on Specification and Design Languages

A2 - Morawiec, Adam

A2 - Hinderscheit, Jinnie

PB - IEEE

T2 - 2012 Forum on specification & Design Languages

Y2 - 18 September 2012 through 20 September 2012

ER -