ReWire is a programming language designed to support a purely functional style
of hardware design. Previous research has demonstrated the efficacy of ReWire
as a hardware design language, and that ReWire provides a powerful framework
for verification via simple ""Bird-Wadler"" style equational reasoning. In this
talk, I will discuss ongoing effors to mechanize the metatheory of ReWire in
Coq, including proofs of type safety, strong normalization, and the soundness
of ReWire's equational theory.