| 2024 | RSP | Temporal Staging for Correct-by-Construction Cryptographic Hardware. | Yakir Forman, William L. Harrison |
| 2021 | PPDP | A Mechanized Semantic Metalanguage for High Level Synthesis. | William L. Harrison, Chris Hathhorn, Gerard Allwein |
| 2020 | DATE | Verifiable Security Templates for Hardware. | William L. Harrison, Gerard Allwein |
| 2020 | ICFP | Strongly bounded termination with applications to security and hardware synthesis. | Thomas N. Reynolds, William L. Harrison, Rohit Chadha, Gerard Allwein |
| 2018 | RSP | Semantics-Directed Prototyping of Hardware Runtime Monitors. | William L. Harrison, Gerard Allwein |
| 2017 | MEMOCODE | A core calculus for secure hardware: its formal semantics and proof system. | Thomas N. Reynolds, Adam M. Procter, William L. Harrison, Gerard Allwein |
| 2016 | RSP | Model-driven design & synthesis of the SHA-256 cryptographic hash function in rewire. | William L. Harrison, Adam M. Procter, Gerard Allwein |
| 2012 | ICFEM | The Confinement Problem in the Presence of Faults. | William L. Harrison, Adam M. Procter, Gerard Allwein |
| 2010 | AiML | Partially-ordered Modalities. | Gerard Allwein, William L. Harrison |
| 2008 | HASKELL | Making monads first-class with template haskell. | Pericles S. Kariotis, Adam M. Procter, William L. Harrison |
| 2008 | MPC | Asynchronous Exceptions as an Effect. | William L. Harrison, Gerard Allwein, Andy Gill, Adam M. Procter |
| 2006 | APLAS | Proof Abstraction for Imperative Languages. | William L. Harrison |
| 2005 | APLAS | A Simple Semantics for Polymorphic Recursion. | William L. Harrison |
| 2005 | BIBE | RNA Pseudoknot Prediction Using Term Rewriting. | Xuezheng Fu, Hao Wang, William L. Harrison, Robert W. Harrison |
| 2002 | MPC | Fine Control of Demand in Haskell. | William L. Harrison, Tim Sheard, James Hook |
| 2000 | MPC | Metacomputation-Based Compiler Architecture. | William L. Harrison, Samuel N. Kamin |