| 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 |
| 2013 | CISS | Capacity of an intensity interferometry channel. | Pedro N. Safier, Ira S. Moskowitz, 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 | MPC | Asynchronous Exceptions as an Effect. | William L. Harrison, Gerard Allwein, Andy Gill, Adam M. Procter |
| 2004 | DIAGRAMS | Diagrams and Non-monotonicity in Puzzles. | Benedek Nagy, Gerard Allwein |
| 2004 | NSPW | A qualitative framework for Shannon information theories. | Gerard Allwein |
| 2002 | DIAGRAMS | Modeling Heterogeneous Systems. | Nik Swoboda, Gerard Allwein |