| 2018 | PPDP | Semantic Equivalence Checking for HHVM Bytecode. | Nick Benton |
| 2016 | PPDP | Effect-dependent transformations for concurrent programs. | Nick Benton, Martin Hofmann, Vivek Nigam |
| 2015 | POPL | Integrating Linear and Dependent Types. | Neelakantan R. Krishnaswami, Ccilia Pradic, Nick Benton |
| 2014 | POPL | Abstract effects and proof-relevant logical relations. | Nick Benton, Martin Hofmann, Vivek Nigam |
| 2013 | APLAS | The Proof Assistant as an Integrated Development Environment. | Nick Benton |
| 2013 | POPL | High-level separation logic for low-level code. | Jonas Braband Jensen, Nick Benton, Andrew Kennedy |
| 2013 | PPDP | Coq: the world's best macro assembler? | Andrew Kennedy, Nick Benton, Jonas Braband Jensen, Pierre-variste Dagand |
| 2012 | ESOP | Adding Equations to System F Types. | Neelakantan R. Krishnaswami, Nick Benton |
| 2012 | POPL | Higher-order functional reactive programming in bounded space. | Neelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann |
| 2011 | ICFP | A semantic model for graphical user interfaces. | Neelakantan R. Krishnaswami, Nick Benton |
| 2011 | LICS | Ultrametric Semantics of Reactive Programs. | Neelakantan R. Krishnaswami, Nick Benton |
| 2009 | ICFP | Biorthogonality, step-indexing and compiler correctness. | Nick Benton, Chung-Kil Hur |
| 2009 | PPDP | Relational semantics for effect-based program transformations: higher-order store. | Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann |
| 2008 | DIAGRAMS | Diagrammatic Reasoning in Separation Logic. | M. Ridsdale, Mateja Jamnik, Nick Benton, Josh Berdine |
| 2008 | FLOPS | Undoing Dynamic Typing (Declarative Pearl). | Nick Benton |
| 2007 | PPDP | Relational semantics for effect-based program transformations with dynamic allocation. | Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann |
| 2007 | PPDP | Formalizing and verifying semantic type soundness of a simple compiler. | Nick Benton, Uri Zarfaty |
| 2006 | APLAS | Reading, Writing and Relations. | Nick Benton, Andrew Kennedy, Martin Hofmann, Lennart Beringer |
| 2006 | CSL | Abstracting Allocation. | Nick Benton |
| 2005 | APLAS | A Typed, Compositional Logic for a Stack-Based Abstract Machine. | Nick Benton |
| 2004 | POPL | Simple relational correctness proofs for static analyses and program transformations. | Nick Benton |
| 2004 | PPDP | Adventures in interoperability: the SML.NET experience. | Nick Benton, Andrew Kennedy, Claudio V. Russo |
| 2002 | ECOOP | Modern Concurrency Abstractions for C | Nick Benton, Luca Cardelli, Cdric Fournet |
| 1999 | ICFP | Interlanguage Working Without Tears: Blending SML with Java. | Nick Benton, Andrew Kennedy |
| 1998 | ICFP | Compiling Standard ML to Java Bytecodes. | Nick Benton, Andrew Kennedy, George Russell |