| 2019 | SP | The Code That Never Ran: Modeling Attacks on Speculative Evaluation. | Craig Disselkoen, Radha Jagadeesan, Alan Jeffrey, James Riely |
| 2016 | LICS | On Thin Air Reads Towards an Event Structures Model of Relaxed Memory. | Alan Jeffrey, James Riely |
| 2014 | CSL | Functional reactive types. | Alan Jeffrey |
| 2013 | ICFP | Functional reactive programming with liveness guarantees. | Alan Jeffrey |
| 2013 | ICWS | Validation and Interactivity of Web API Documentation. | Peter J. Danielsen, Alan Jeffrey |
| 2013 | PADL | Dependently Typed Web Client Applications - FRP in Agda in HTML5. | Alan Jeffrey |
| 2011 | CSL | The Lax Braided Structure of Streaming I/O. | Alan Jeffrey, Julian Rathke |
| 2011 | POPL | Robin Milner 1934--2010: verification, languages, and concurrency. | Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell |
| 2009 | ESORICS | Towards a Theory of Accountability and Audit. | Radha Jagadeesan, Alan Jeffrey, Corin Pitcher, James Riely |
| 2008 | SIGMOD | Stream firewalling of xml constraints. | Michael Benedikt, Alan Jeffrey, Ruy Ley-Wild |
| 2006 | ICALP | Untitled record | Radha Jagadeesan, Alan Jeffrey, Corin Pitcher, James Riely |
| 2005 | CONCUR | Secrecy Despite Compromise: Types, Cryptography, and the Pi-Calculus. | Andrew D. Gordon, Alan Jeffrey |
| 2005 | CONCUR | Timed Spi-Calculus with Types for Secrecy and Authenticity. | Christian Haack, Alan Jeffrey |
| 2005 | ESOP | Java Jr: Fully Abstract Trace Semantics for a Core Java Language. | Alan Jeffrey, Julian Rathke |
| 2005 | FOSSACS | Full Abstraction for Polymorphic Pi-Calculus. | Alan Jeffrey, Julian Rathke |
| 2004 | CONCUR | ABC: A Minimal Aspect Calculus. | Glenn Bruns, Radha Jagadeesan, Alan Jeffrey, James Riely |
| 2003 | ECOOP | A Calculus of Untyped Aspect-Oriented Programs. | Radha Jagadeesan, Alan Jeffrey, James Riely |
| 2003 | MFPS | Contextual Equivalence for Higher-Order π-Calculus Revisited. | Alan Jeffrey, Julian Rathke |
| 2002 | LICS | A Fully Abstract May Testing Semantics for Concurrent Objects. | Alan Jeffrey, Julian Rathke |
| 2001 | LICS | A Symbolic Labelled Transition System for Coinductive Subtyping of | Alan Jeffrey |
| 2001 | SAS | A Type and Effect Analysis of Security Protocols. | Andrew D. Gordon, Alan Jeffrey |
| 2000 | LICS | A Theory of Bisimulation for a Fragment of Concurrent ML with Local Names. | Alan Jeffrey, Julian Rathke |
| 1999 | LICS | Towards a Theory of Bisimulation for Local Names. | Alan Jeffrey, Julian Rathke |
| 1996 | ICFP | A Theory of Weak Bisimulation for Core CML. | William Ferreira, Matthew Hennessy, Alan Jeffrey |
| 1995 | LICS | A Fully Abstract Semantics for a Concurrent Functional Language with Monadic Types | Alan Jeffrey |
| 1994 | LFCS | Allegories of Circuits. | Carolyn Brown, Alan Jeffrey |
| 1994 | LICS | A Fully Abstract Semantics for Concurrent Graph Reduction | Alan Jeffrey |
| 1993 | MFPS | A Chemical Abstract Machine for Graph Reduction. | Alan Jeffrey |
| 1991 | CAV | A Linear Time Process Algebra. | Alan Jeffrey |
| 1991 | CONCUR | Abstract Timed Observation and Process Algebra. | Alan Jeffrey |