A core calculus for secure hardware: its formal semantics and proof system. - Thomas N. Reynolds; Adam M. Procter; William L. Harrison; Gerard Allwein (MEMOCODE, 2017)

The Mechanized Marriage of Effects and Monads with Applications to High-assurance Hardware. - Thomas N. Reynolds; Adam M. Procter; William L. Harrison; Gerard Allwein (ACM Trans. Embed. Comput. Syst., 2019)

Strongly bounded termination with applications to security and hardware synthesis. - Thomas N. Reynolds; William L. Harrison; Rohit Chadha; Gerard Allwein (TyDe@ICFP, 2020)