|START Conference Manager|
We develop a variant of the lambda calculus, called $\lang$ (linear lambda), which may serve as a high-level substitute for netlists. In order to support higher-order functions, $\lang$ uses a linear type system which enforces the linear use of variables of function type. The translation of $\lang$ into structural descriptions of hardware circuits is sound and complete in the sense that it maps expressions only to realizable hardware circuits and that every realizable hardware circuit has a corresponding expression in $\lang$. To illustrate the use of $\lang$ as a high-level substitute for netlists, we design a simple hardware description language that extends $\lang$ with polymorphism, and use it to implement a Fast Fourier Transform circuit.
START Conference Manager (V2.54.6)