A functional language for describing reversible logic
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Standard
A functional language for describing reversible logic. / Thomsen, Michael Kirkedal.
Proceedings of the 2012 Forum on Specification and Design Languages. red. / Adam Morawiec; Jinnie Hinderscheit. IEEE, 2012. s. 135-142.Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
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
Y2 - 18 September 2012 through 20 September 2012
ER -
ID: 40367802