Linear Lambda-Calculus and Categorial Models Revisited. - P. N. Benton; Gavin M. Bierman; Valeria de Paiva; Martin Hyland (CSL, 1992)

Strictness Logic and Polymorphic Invariance. - P. N. Benton (LFCS, 1992)

Strictness Properties of Lazy Algebraic Datatypes. - P. N. Benton (WSA, 1993)

A Term Calculus for Intuitionistic Linear Logic. - P. N. Benton; Gavin M. Bierman; Valeria de Paiva; Martin Hyland (TLCA, 1993)

A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). - P. N. Benton (CSL, 1994)

Strong Normalisation for the Linear Term Calculus. - P. N. Benton (J. Funct. Program., 1995)

Linear Logic, Monads and the Lambda Calculus. - P. N. Benton; Philip Wadler (LICS, 1996)

On the Relationship Between Formal Semantics and Static Analysis. - P. N. Benton (ACM Comput. Surv., 1996)

Compiling Standard ML to Java Bytecodes. - Nick Benton; Andrew Kennedy; George Russell (ICFP, 1998)

Computational Types from a Logical Perspective. - P. N. Benton; Gavin M. Bierman; Valeria de Paiva (J. Funct. Program., 1998)

Interlanguage Working Without Tears: Blending SML with Java. - Nick Benton; Andrew Kennedy (ICFP, 1999)

Monads, Effects and Transformations. - Nick Benton; Andrew Kennedy (HOOTS, 1999)

Monads and Effects. - Nick Benton; John Hughes 001; Eugenio Moggi (APPSEM, 2000)

Type inference for MLj. - Bruce J. McAdam; Andrew Kennedy; Nick Benton (Scottish Functional Programming Workshop, 2000)

Exceptional Syntax Journal of Functional Programming. - Nick Benton; Andrew Kennedy (J. Funct. Program., 2001)

BABEL 2001 - Preface. - Nick Benton; Andrew Kennedy (BABEL, 2001)

Modern Concurrency Abstractions for C#. - Nick Benton; Luca Cardelli; Cédric Fournet (ECOOP, 2002)

Traced pre-monoidal categories. - Nick Benton; Martin Hyland (FICS, 2002)

Traced Premonoidal Categories. - Nick Benton; Martin Hyland (RAIRO Theor. Informatics Appl., 2003)

Shrinking Reductions in SML.NET. - Nick Benton; Andrew Kennedy; Sam Lindley; Claudio V. Russo (IFL, 2004)

Simple relational correctness proofs for static analyses and program transformations. - Nick Benton (POPL, 2004)

Adventures in interoperability: the SML.NET experience. - Nick Benton; Andrew Kennedy; Claudio V. Russo (PPDP, 2004)

Modern concurrency abstractions for C#. - Nick Benton; Luca Cardelli; Cédric Fournet (ACM Trans. Program. Lang. Syst., 2004)

A Typed, Compositional Logic for a Stack-Based Abstract Machine. - Nick Benton (APLAS, 2005)

Relational Reasoning in a Nominal Semantics for Storage. - Nick Benton; Benjamin Leperchey (TLCA, 2005)

Preface. - Nick Benton; Xavier Leroy (ML, 2005)

Embedded interpreters. - Nick Benton (J. Funct. Program., 2005)

Reading, Writing and Relations. - Nick Benton; Andrew Kennedy; Martin Hofmann 001; Lennart Beringer (APLAS, 2006)

Abstracting Allocation. - Nick Benton (CSL, 2006)

Relational semantics for effect-based program transformations with dynamic allocation. - Nick Benton; Andrew Kennedy; Lennart Beringer; Martin Hofmann 001 (PPDP, 2007)

Formalizing and verifying semantic type soundness of a simple compiler. - Nick Benton; Uri Zarfaty (PPDP, 2007)

Semantics of an effect analysis for exceptions. - Nick Benton; Peter Buchlovsky (TLDI, 2007)

08061 Executive Summary – Types, Logics and Semantics for State. - Amal Ahmed 001; Nick Benton; Martin Hofmann 001; Greg Morrisett (Types, Logics and Semantics for State, 2008)

08061 Abstracts Collection – Types, Logics and Semantics for State. - Amal Ahmed 001; Nick Benton; Martin Hofmann 001; Greg Morrisett (Types, Logics and Semantics for State, 2008)

Diagrammatic Reasoning in Separation Logic. - M. Ridsdale; Mateja Jamnik; Nick Benton; Josh Berdine (Diagrams, 2008)

Undoing Dynamic Typing (Declarative Pearl). - Nick Benton (FLOPS, 2008)

Biorthogonality, step-indexing and compiler correctness. - Nick Benton; Chung-Kil Hur (ICFP, 2009)

Relational semantics for effect-based program transformations: higher-order store. - Nick Benton; Andrew Kennedy; Lennart Beringer; Martin Hofmann 001 (PPDP, 2009)

Compiling functional types to relational specifications for low level imperative code. - Nick Benton; Nicolas Tabareau (TLDI, 2009)

Some Domain Theory and Denotational Semantics in Coq. - Nick Benton; Andrew Kennedy; Carsten Varming (TPHOLs, 2009)

10351 Abstracts Collection - Modelling, Controlling and Reasoning About State. - Amal Ahmed 001; Nick Benton; Lars Birkedal; Martin Hofmann 001 (Modelling, Controlling and Reasoning About State, 2010)

10351 Executive Summary - Modelling, Controlling and Reasoning About State. - Amal Ahmed 001; Nick Benton; Lars Birkedal; Martin Hofmann 001 (Modelling, Controlling and Reasoning About State, 2010)

Step-Indexing: The Good, the Bad and the Ugly. - Nick Benton; Chung-Kil Hur (Modelling, Controlling and Reasoning About State, 2010)

A semantic model for graphical user interfaces. - Neelakantan R. Krishnaswami; Nick Benton (ICFP, 2011)

Ultrametric Semantics of Reactive Programs. - Neelakantan R. Krishnaswami; Nick Benton (LICS, 2011)

Adding Equations to System F Types. - Neelakantan R. Krishnaswami; Nick Benton (ESOP, 2012)

Higher-order functional reactive programming in bounded space. - Neelakantan R. Krishnaswami; Nick Benton; Jan Hoffmann 002 (POPL, 2012)

Strongly Typed Term Representations in Coq. - Nick Benton; Chung-Kil Hur; Andrew Kennedy; Conor McBride (J. Autom. Reason., 2012)

The Proof Assistant as an Integrated Development Environment. - Nick Benton (APLAS, 2013)

High-level separation logic for low-level code. - Jonas Braband Jensen; Nick Benton; Andrew Kennedy (POPL, 2013)

Coq: the world's best macro assembler? - Andrew Kennedy; Nick Benton; Jonas Braband Jensen; Pierre-Évariste Dagand (PPDP, 2013)

Abstract effects and proof-relevant logical relations. - Nick Benton; Martin Hofmann 001; Vivek Nigam (POPL, 2014)

Integrating Linear and Dependent Types. - Neelakantan R. Krishnaswami; Cécilia Pradic; Nick Benton (POPL, 2015)

Counting Successes: Effects and Transformations for Non-deterministic Programs. - Nick Benton; Andrew Kennedy; Martin Hofmann 001; Vivek Nigam (A List of Successes That Can Change the World, 2016)

Correctness of compiling polymorphism to dynamic typing. - Kuen-Bang Hou (Favonia); Nick Benton; Robert Harper 001 (J. Funct. Program., 2017)

Semantic Equivalence Checking for HHVM Bytecode. - Nick Benton (PPDP, 2018)

Proof-Relevant Logical Relations for Name Generation. - Nick Benton; Martin Hofmann 001; Vivek Nigam (Log. Methods Comput. Sci., 2018)

Effect-dependent transformations for concurrent programs. - Nick Benton; Martin Hofmann 001; Vivek Nigam (Sci. Comput. Program., 2018)