Nick Benton

Publication Activity (10 Years)

Years Active: 1998-2018
Publications (10 Years): 7

Top Topics

Theorem Proving

Concurrent Programs

Relevant Concepts

High Level Abstractions

Top Venues

J. Funct. Program.

Publications

Nick Benton
Semantic Equivalence Checking for HHVM Bytecode. PPDP (2018)
Nick Benton, Martin Hofmann, Vivek Nigam
Proof-Relevant Logical Relations for Name Generation. Log. Methods Comput. Sci. 14 (1) (2018)
Nick Benton, Martin Hofmann, Vivek Nigam
Effect-dependent transformations for concurrent programs. Sci. Comput. Program. 155 (2018)
Kuen-Bang Hou (Favonia), Nick Benton, Robert Harper
Correctness of compiling polymorphism to dynamic typing. J. Funct. Program. 27 (2017)
Nick Benton, Martin Hofmann, Vivek Nigam
Proof-Relevant Logical Relations for Name Generation. CoRR (2017)
Nick Benton, Andrew Kennedy, Martin Hofmann, Vivek Nigam
Counting Successes: Effects and Transformations for Non-deterministic Programs. A List of Successes That Can Change the World (2016)
Nick Benton, Martin Hofmann, Vivek Nigam
Effect-dependent transformations for concurrent programs. PPDP (2016)
Neelakantan R. Krishnaswami, Pierre Pradic, Nick Benton
Integrating Linear and Dependent Types. POPL (2015)
Nick Benton, Martin Hofmann, Vivek Nigam
Effect-Dependent Transformations for Concurrent Programs. CoRR (2015)
Nick Benton, Martin Hofmann, Vivek Nigam
Abstract effects and proof-relevant logical relations. POPL (2014)
Andrew Kennedy, Nick Benton, Jonas Braband Jensen, Pierre-Évariste Dagand
Coq: the world's best macro assembler? PPDP (2013)
Nick Benton
The Proof Assistant as an Integrated Development Environment. APLAS (2013)
Nick Benton, Martin Hofmann, Vivek Nigam
Proof-Relevant Logical Relations for Name Generation. TLCA (2013)
Jonas Braband Jensen, Nick Benton, Andrew Kennedy
High-level separation logic for low-level code. POPL (2013)
Neelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann
Higher-order functional reactive programming in bounded space. POPL (2012)
Neelakantan R. Krishnaswami, Nick Benton
Adding Equations to System F Types. ESOP (2012)
Nick Benton, Martin Hofmann, Vivek Nigam
Abstract Effects and Proof-Relevant Logical Relations CoRR (2012)
Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride
Strongly Typed Term Representations in Coq. J. Autom. Reason. 49 (2) (2012)
Neelakantan R. Krishnaswami, Nick Benton
A semantic model for graphical user interfaces. ICFP (2011)
Neelakantan R. Krishnaswami, Nick Benton
Ultrametric Semantics of Reactive Programs. LICS (2011)
Nick Benton, Chung-Kil Hur
Step-Indexing: The Good, the Bad and the Ugly. Modelling, Controlling and Reasoning About State (2010)
Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann
10351 Executive Summary - Modelling, Controlling and Reasoning About State. Modelling, Controlling and Reasoning About State (2010)
Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann
10351 Abstracts Collection - Modelling, Controlling and Reasoning About State. Modelling, Controlling and Reasoning About State (2010)
Nick Benton, Nicolas Tabareau
Compiling functional types to relational specifications for low level imperative code. TLDI (2009)
Nick Benton, Chung-Kil Hur
Biorthogonality, step-indexing and compiler correctness. ICFP (2009)
Nick Benton, Andrew Kennedy, Carsten Varming
Some Domain Theory and Denotational Semantics in Coq. TPHOLs (2009)
Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann
Relational semantics for effect-based program transformations: higher-order store. PPDP (2009)
M. Ridsdale, Mateja Jamnik, Nick Benton, Josh Berdine
Diagrammatic Reasoning in Separation Logic. Diagrams (2008)
Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett
08061 Abstracts Collection -- Types, Logics and Semantics for State. Types, Logics and Semantics for State (2008)
Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett
08061 Executive Summary -- Types, Logics and Semantics for State. Types, Logics and Semantics for State (2008)
Nick Benton
Undoing Dynamic Typing (Declarative Pearl). FLOPS (2008)
Nick Benton, Peter Buchlovsky
Semantics of an effect analysis for exceptions. TLDI (2007)
Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann
Relational semantics for effect-based program transformations with dynamic allocation. PPDP (2007)
Nick Benton, Uri Zarfaty
Formalizing and verifying semantic type soundness of a simple compiler. PPDP (2007)
Nick Benton, Xavier Leroy
Preface. Electron. Notes Theor. Comput. Sci. 148 (2) (2006)
Nick Benton
Abstracting Allocation. CSL (2006)
Nick Benton, Andrew Kennedy, Martin Hofmann, Lennart Beringer
Reading, Writing and Relations. APLAS (2006)
Nick Benton
A Typed, Compositional Logic for a Stack-Based Abstract Machine. APLAS (2005)
Nick Benton
Embedded interpreters. J. Funct. Program. 15 (4) (2005)
Nick Benton, Benjamin Leperchey
Relational Reasoning in a Nominal Semantics for Storage. TLCA (2005)
Nick Benton, Andrew Kennedy, Claudio V. Russo
Adventures in interoperability: the SML.NET experience. PPDP (2004)
Nick Benton, Andrew Kennedy, Sam Lindley, Claudio V. Russo
Shrinking Reductions in SML.NET. IFL (2004)
Nick Benton, Luca Cardelli, Cédric Fournet
Modern concurrency abstractions for C#. ACM Trans. Program. Lang. Syst. 26 (5) (2004)
Nick Benton
Simple relational correctness proofs for static analyses and program transformations. POPL (2004)
Nick Benton, Martin Hyland
Traced Premonoidal Categories. RAIRO Theor. Informatics Appl. 37 (4) (2003)
Nick Benton, Luca Cardelli, Cédric Fournet
. ECOOP (2002)
Nick Benton, Martin Hyland
Traced pre-monoidal categories. FICS (2002)
Nick Benton, Andrew Kennedy
Exceptional Syntax Journal of Functional Programming. J. Funct. Program. 11 (4) (2001)
Nick Benton, Andrew Kennedy
BABEL 2001 - Preface. Electron. Notes Theor. Comput. Sci. 59 (1) (2001)
Bruce J. McAdam, Andrew Kennedy, Nick Benton
Type inference for MLj. Scottish Functional Programming Workshop (2000)
Nick Benton, John Hughes, Eugenio Moggi
Monads and Effects. APPSEM (2000)
Nick Benton, Andrew Kennedy
Interlanguage Working Without Tears: Blending SML with Java. ICFP (1999)
Nick Benton, Andrew Kennedy
Monads, Effects and Transformations. Electron. Notes Theor. Comput. Sci. 26 (1999)
Nick Benton, Andrew Kennedy, George Russell
Compiling Standard ML to Java Bytecodes. ICFP (1998)