We present a new lambda calculus-like language for hardware description with higher-order functions. We show that separating the types of wires and higher-order constructs lets us avoid the name-sharing problem commonly encountered by functional hardware description languages. Using nominal sets and equivariant functions, we give categorical semantics to the typed language using Markov categories. This keeps wire and circuit terms separate while allowing each to contain free variables of either variety. Furthermore, we prove normalisation and soundness results and implement a proof-of-concept compiler featuring unification-based typed inference, which is able to extract synthesisable Verilog output from a range of examples. The application of Markov categories and nominal techniques to hardware description is novel to the best of our knowledge.

I’m a 3rd year undergraduate student the University of Oxford. My bachelor’s thesis is in the area of probabilistic programming and is being supervised by Sam Staton.