default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDNick Benton
Person information
- affiliation: Microsoft Research
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2021
[e6]Niccolò Veltri, Nick Benton, Silvia Ghilezan
:
PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, Tallinn, Estonia, September 6-8, 2021. ACM 2021, ISBN 978-1-4503-8689-0 [contents]
2010 – 2019
- 2018
- [j11]Nick Benton, Martin Hofmann, Vivek Nigam:
Proof-Relevant Logical Relations for Name Generation. Log. Methods Comput. Sci. 14(1) (2018) - [j10]Nick Benton, Martin Hofmann, Vivek Nigam:
Effect-dependent transformations for concurrent programs. Sci. Comput. Program. 155: 27-51 (2018) - [c44]Nick Benton:
Semantic Equivalence Checking for HHVM Bytecode. PPDP 2018: 3:1-3:8 - 2017
- [j9]Kuen-Bang Hou (Favonia), Nick Benton, Robert Harper:
Correctness of compiling polymorphism to dynamic typing. J. Funct. Program. 27: e1 (2017) - [i8]Nick Benton, Martin Hofmann, Vivek Nigam:
Proof-Relevant Logical Relations for Name Generation. CoRR abs/1708.05193 (2017) - 2016
- [c43]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: 56-72 - [c42]Nick Benton, Martin Hofmann, Vivek Nigam:
Effect-dependent transformations for concurrent programs. PPDP 2016: 188-201 - 2015
- [c41]Neelakantan R. Krishnaswami, Cécilia Pradic, Nick Benton:
Integrating Linear and Dependent Types. POPL 2015: 17-30 - [i7]Nick Benton, Martin Hofmann, Vivek Nigam:
Effect-Dependent Transformations for Concurrent Programs. CoRR abs/1510.02419 (2015) - 2014
- [c40]Nick Benton, Martin Hofmann, Vivek Nigam:
Abstract effects and proof-relevant logical relations. POPL 2014: 619-632 - 2013
- [c39]Nick Benton:
The Proof Assistant as an Integrated Development Environment. APLAS 2013: 307-314 - [c38]Jonas Braband Jensen, Nick Benton, Andrew Kennedy:
High-level separation logic for low-level code. POPL 2013: 301-314 - [c37]Andrew Kennedy, Nick Benton, Jonas Braband Jensen, Pierre-Évariste Dagand:
Coq: the world's best macro assembler? PPDP 2013: 13-24 - [c36]Nick Benton, Martin Hofmann, Vivek Nigam:
Proof-Relevant Logical Relations for Name Generation. TLCA 2013: 48-60 - 2012
- [j8]Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride:
Strongly Typed Term Representations in Coq. J. Autom. Reason. 49(2): 141-159 (2012) - [c35]Neelakantan R. Krishnaswami, Nick Benton:
Adding Equations to System F Types. ESOP 2012: 417-435 - [c34]Neelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann:
Higher-order functional reactive programming in bounded space. POPL 2012: 45-58 - [i6]Nick Benton, Martin Hofmann, Vivek Nigam:
Abstract Effects and Proof-Relevant Logical Relations. CoRR abs/1212.5692 (2012) - 2011
- [c33]Neelakantan R. Krishnaswami, Nick Benton:
A semantic model for graphical user interfaces. ICFP 2011: 45-57 - [c32]Neelakantan R. Krishnaswami, Nick Benton:
Ultrametric Semantics of Reactive Programs. LICS 2011: 257-266 - 2010
- [e5]Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann:
Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010. Dagstuhl Seminar Proceedings 10351, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany 2010 [contents] - [e4]Andrew Kennedy, Nick Benton:
Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Madrid, Spain, January 23, 2010. ACM 2010, ISBN 978-1-60558-891-9 [contents] - [i5]Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann:
10351 Abstracts Collection - Modelling, Controlling and Reasoning About State. Modelling, Controlling and Reasoning About State 2010 - [i4]Amal Ahmed, Nick Benton, Lars Birkedal, Martin Hofmann:
10351 Executive Summary - Modelling, Controlling and Reasoning About State. Modelling, Controlling and Reasoning About State 2010 - [i3]Nick Benton, Chung-Kil Hur:
Step-Indexing: The Good, the Bad and the Ugly. Modelling, Controlling and Reasoning About State 2010
2000 – 2009
- 2009
- [c31]Nick Benton, Chung-Kil Hur:
Biorthogonality, step-indexing and compiler correctness. ICFP 2009: 97-108 - [c30]Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann:
Relational semantics for effect-based program transformations: higher-order store. PPDP 2009: 301-312 - [c29]Nick Benton, Nicolas Tabareau:
Compiling functional types to relational specifications for low level imperative code. TLDI 2009: 3-14 - [c28]Nick Benton, Andrew Kennedy, Carsten Varming:
Some Domain Theory and Denotational Semantics in Coq. TPHOLs 2009: 115-130 - 2008
- [c27]M. Ridsdale, Mateja Jamnik, Nick Benton, Josh Berdine:
Diagrammatic Reasoning in Separation Logic. Diagrams 2008: 408-411 - [c26]Nick Benton:
Undoing Dynamic Typing (Declarative Pearl). FLOPS 2008: 224-238 - [e3]Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett:
Types, Logics and Semantics for State, 03.02. - 08.02.2008. Dagstuhl Seminar Proceedings 08061, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2008 [contents] - [i2]Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett:
08061 Executive Summary -- Types, Logics and Semantics for State. Types, Logics and Semantics for State 2008 - [i1]Amal Ahmed, Nick Benton, Martin Hofmann, Greg Morrisett:
08061 Abstracts Collection -- Types, Logics and Semantics for State. Types, Logics and Semantics for State 2008 - 2007
- [c25]Nick Benton, Uri Zarfaty:
Formalizing and verifying semantic type soundness of a simple compiler. PPDP 2007: 1-12 - [c24]Nick Benton, Andrew Kennedy, Lennart Beringer, Martin Hofmann:
Relational semantics for effect-based program transformations with dynamic allocation. PPDP 2007: 87-96 - [c23]Nick Benton, Peter Buchlovsky:
Semantics of an effect analysis for exceptions. TLDI 2007: 15-26 - 2006
- [c22]Nick Benton, Andrew Kennedy, Martin Hofmann, Lennart Beringer:
Reading, Writing and Relations. APLAS 2006: 114-130 - [c21]Nick Benton:
Abstracting Allocation. CSL 2006: 182-196 - [e2]Nick Benton, Xavier Leroy:
Proceedings of the ACM-SIGPLAN Workshop on ML, ML 2005, Tallinn, Estonia, September 29, 2005. Electronic Notes in Theoretical Computer Science 148(2), Elsevier 2006 [contents] - 2005
- [j7]Nick Benton:
Embedded interpreters. J. Funct. Program. 15(4): 503-542 (2005) - [c20]Nick Benton:
A Typed, Compositional Logic for a Stack-Based Abstract Machine. APLAS 2005: 364-380 - [c19]Nick Benton, Benjamin Leperchey:
Relational Reasoning in a Nominal Semantics for Storage. TLCA 2005: 86-101 - [c18]Nick Benton, Xavier Leroy:
Preface. ML 2005: 1-2 - 2004
- [j6]Nick Benton, Luca Cardelli, Cédric Fournet:
Modern concurrency abstractions for C#. ACM Trans. Program. Lang. Syst. 26(5): 769-804 (2004) - [c17]Nick Benton, Andrew Kennedy, Sam Lindley, Claudio V. Russo:
Shrinking Reductions in SML.NET. IFL 2004: 142-159 - [c16]Nick Benton:
Simple relational correctness proofs for static analyses and program transformations. POPL 2004: 14-25 - [c15]Nick Benton, Andrew Kennedy, Claudio V. Russo:
Adventures in interoperability: the SML.NET experience. PPDP 2004: 215-226 - 2003
- [j5]Nick Benton, Martin Hyland:
Traced Premonoidal Categories. RAIRO Theor. Informatics Appl. 37(4): 273-299 (2003) - 2002
- [c14]Nick Benton, Luca Cardelli, Cédric Fournet:
Modern Concurrency Abstractions for C#. ECOOP 2002: 415-440 - [c13]Nick Benton, Martin Hyland:
Traced pre-monoidal categories. FICS 2002: 12-19 - 2001
- [j4]Nick Benton, Andrew Kennedy:
Exceptional Syntax Journal of Functional Programming. J. Funct. Program. 11(4): 395-410 (2001) - [c12]Nick Benton, Andrew Kennedy:
BABEL 2001 - Preface. BABEL 2001: 1 - [e1]Nick Benton, Andrew Kennedy:
First International Workshop on Multi-Language Infrastructure and Interoperability, BABEL 2001, Satellite Event of PLI 2001, Firenze, Italy, September 8, 2001. Electronic Notes in Theoretical Computer Science 59(1), Elsevier 2001 [contents] - 2000
- [c11]Nick Benton, John Hughes, Eugenio Moggi:
Monads and Effects. APPSEM 2000: 42-122 - [c10]Bruce J. McAdam, Andrew Kennedy, Nick Benton:
Type inference for MLj. Scottish Functional Programming Workshop 2000: 159-172
1990 – 1999
- 1999
- [c9]Nick Benton, Andrew Kennedy:
Interlanguage Working Without Tears: Blending SML with Java. ICFP 1999: 126-137 - [c8]Nick Benton, Andrew Kennedy:
Monads, Effects and Transformations. HOOTS 1999: 3-20 - 1998
- [j3]P. N. Benton, Gavin M. Bierman, Valeria de Paiva:
Computational Types from a Logical Perspective. J. Funct. Program. 8(2): 177-193 (1998) - [c7]Nick Benton, Andrew Kennedy, George Russell:
Compiling Standard ML to Java Bytecodes. ICFP 1998: 129-140 - 1996
- [j2]P. N. Benton:
On the Relationship Between Formal Semantics and Static Analysis. ACM Comput. Surv. 28(2): 321-323 (1996) - [c6]P. N. Benton, Philip Wadler:
Linear Logic, Monads and the Lambda Calculus. LICS 1996: 420-431 - 1995
- [j1]P. N. Benton:
Strong Normalisation for the Linear Term Calculus. J. Funct. Program. 5(1): 65-80 (1995) - 1994
- [c5]P. N. Benton:
A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). CSL 1994: 121-135 - 1993
- [c4]P. N. Benton:
Strictness Properties of Lazy Algebraic Datatypes. WSA 1993: 206-217 - [c3]P. N. Benton, Gavin M. Bierman, Valeria de Paiva, Martin Hyland:
A Term Calculus for Intuitionistic Linear Logic. TLCA 1993: 75-90 - 1992
- [c2]P. N. Benton, Gavin M. Bierman, Valeria de Paiva, Martin Hyland:
Linear Lambda-Calculus and Categorial Models Revisited. CSL 1992: 61-84 - [c1]P. N. Benton:
Strictness Logic and Polymorphic Invariance. LFCS 1992: 33-44
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 22:48 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
