Travelled to:1 × Canada
1 × Estonia
1 × France
1 × Germany
1 × Hungary
1 × India
1 × Poland
1 × Portugal
1 × The Netherlands
1 × United Kingdom
2 × Spain
3 × Italy
3 × Japan
3 × USA
Collaborated with:A.Kennedy N.R.Krishnaswami ∅ M.Hofmann V.Nigam J.B.Jensen C.V.Russo C.Hur L.Beringer U.Zarfaty B.Leperchey P.Pradic J.Hoffmann L.Cardelli C.Fournet G.Russell M.H.0001 P.Dagand S.Lindley
Talks about:semant (7) program (6) relat (6) transform (4) effect (4) type (4) abstract (3) compil (3) proof (3) logic (3)
Person: Nick Benton
DBLP: Benton:Nick
Contributed to:
201520142013
2013
2013
20122012
2011
201120092009
20082007
20062005
200420042004
20021999199820162018Wrote 24 papers:
- POPL-2015-KrishnaswamiPB #dependent type #linear
- Integrating Linear and Dependent Types (NRK, PP, NB), pp. 17–30.
- POPL-2014-Benton0N #logic
- Abstract effects and proof-relevant logical relations (NB, MH, VN), pp. 619–632.
- POPL-2013-JensenBK #logic #low level
- High-level separation logic for low-level code (JBJ, NB, AK), pp. 301–314.
- PPDP-2013-KennedyBJD #assembly #coq #metaprogramming #named #question
- Coq: the world’s best macro assembler? (AK, NB, JBJ, PÉD), pp. 13–24.
- TLCA-2013-BentonHN #generative #logic
- Proof-Relevant Logical Relations for Name Generation (NB, MH, VN), pp. 48–60.
- ESOP-2012-KrishnaswamiB #equation #system f
- Adding Equations to System F Types (NRK, NB), pp. 417–435.
- POPL-2012-KrishnaswamiBH #bound #functional #higher-order #programming
- Higher-order functional reactive programming in bounded space (NRK, NB, JH), pp. 45–58.
- ICFP-2011-KrishnaswamiB #semantics #user interface #visual notation
- A semantic model for graphical user interfaces (NRK, NB), pp. 45–57.
- LICS-2011-KrishnaswamiB #semantics #source code
- Ultrametric Semantics of Reactive Programs (NRK, NB), pp. 257–266.
- ICFP-2009-BentonH #compilation #correctness
- Biorthogonality, step-indexing and compiler correctness (NB, CKH), pp. 97–108.
- PPDP-2009-BentonKBH #higher-order #program transformation #relational #semantics
- Relational semantics for effect-based program transformations: higher-order store (NB, AK, LB, MH), pp. 301–312.
- FLOPS-2008-Benton #dynamic typing #type system
- Undoing Dynamic Typing (NB), pp. 224–238.
- PPDP-2007-BentonKBH #program transformation #relational #semantics
- Relational semantics for effect-based program transformations with dynamic allocation (NB, AK, LB, MH), pp. 87–96.
- PPDP-2007-BentonZ #compilation #formal method #semantics #verification
- Formalizing and verifying semantic type soundness of a simple compiler (NB, UZ), pp. 1–12.
- CSL-2006-Benton
- Abstracting Allocation (NB), pp. 182–196.
- TLCA-2005-BentonL #reasoning #relational #semantics
- Relational Reasoning in a Nominal Semantics for Storage (NB, BL), pp. 86–101.
- IFL-2004-BentonKLR #reduction
- Shrinking Reductions in SML.NET (NB, AK, SL, CVR), pp. 142–159.
- POPL-2004-Benton #analysis #correctness #program transformation #proving #relational
- Simple relational correctness proofs for static analyses and program transformations (NB), pp. 14–25.
- PPDP-2004-BentonKR #experience
- Adventures in interoperability: the SML.NET experience (NB, AK, CVR), pp. 215–226.
- ECOOP-2002-BentonCF #abstraction #c# #concurrent
- Modern Concurrency Abstractions for C# (NB, LC, CF), pp. 415–440.
- ICFP-1999-BentonK #java
- Interlanguage Working Without Tears: Blending SML with Java (NB, AK), pp. 126–137.
- ICFP-1998-BentonKR #compilation #java #ml #standard
- Compiling Standard ML to Java Bytecodes (NB, AK, GR), pp. 129–140.
- PPDP-2016-Benton0N #concurrent #source code
- Effect-dependent transformations for concurrent programs (NB, MH0, VN), pp. 188–201.
- PPDP-2018-Benton #bytecode #equivalence #semantics
- Semantic Equivalence Checking for HHVM Bytecode (NB), p. 8.