Making monads first-class with template haskell. - Pericles S. Kariotis; Adam M. Procter; William L. Harrison (Haskell, 2008)

Asynchronous Exceptions as an Effect. - William L. Harrison; Gerard Allwein; Andy Gill; Adam M. Procter (MPC, 2008)

Model-Driven Engineering from Modular Monadic Semantics: Implementation Techniques Targeting Hardware and Software. - William L. Harrison; Adam M. Procter; Jason Agron; Garrin Kimmell; Gerard Allwein (DSL, 2009)

A virtual memory based runtime to support multi-tenancy in clusters with GPUs. - Michela Becchi; Kittisak Sajjapongse; Ian Graves; Adam M. Procter; Vignesh T. Ravi; Srimat T. Chakradhar (HPDC, 2012)

The Confinement Problem in the Presence of Faults. - William L. Harrison; Adam M. Procter; Gerard Allwein (ICFEM, 2012)

The Design of a Practical Proof Checker for a Lazy Functional Language. - Adam M. Procter; William L. Harrison; Aaron Stump (Trends in Functional Programming, 2012)

Formal Semantics of Heterogeneous CUDA-C: A Modular Approach with Applications - Chris Hathhorn; Michela Becchi; William L. Harrison; Adam M. Procter (SSV, 2012)

Semantics-directed machine architecture in ReWire. - Adam M. Procter; William L. Harrison; Ian Graves; Michela Becchi; Gerard Allwein (FPT, 2013)

Hardware Synthesis from Functional Embedded Domain-Specific Languages: A Case Study in Regular Expression Compilation. - Ian Graves; Adam M. Procter; William L. Harrison; Michela Becchi; Gerard Allwein (ARC, 2015)

Provably Correct Development of reconfigurable hardware designs via equational reasoning. - Ian Graves; Adam M. Procter; William L. Harrison; Gerard Allwein (FPT, 2015)

Semantics Driven Hardware Design, Implementation, and Verification with ReWire. - Adam M. Procter; William L. Harrison; Ian Graves; Michela Becchi; Gerard Allwein (LCTES, 2015)

A programming model for reconfigurable computing based in functional concurrency. - William L. Harrison; Ian Graves; Adam M. Procter; Michela Becchi; Gerard Allwein (ReCoSoC, 2016)

Model-driven design & synthesis of the SHA-256 cryptographic hash function in rewire. - William L. Harrison; Adam M. Procter; Gerard Allwein (RSP, 2016)

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)

A Principled Approach to Secure Multi-core Processor Design with ReWire. - Adam M. Procter; William L. Harrison; Ian Graves; Michela Becchi; Gerard Allwein (ACM Trans. Embed. Comput. Syst., 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)