BibSLEIGH — Nikhil

Travelled to:

1 × Canada
1 × Cyprus
1 × India
1 × Italy
1 × Japan
1 × Norway
1 × United Kingdom
5 × USA

Collaborated with:

J.Chen C.Fournet P.Strub A.Rastogi G.M.Bierman R.Chugh M.W.Hicks D.Leijen C.Hritcu K.Bhargavan D.Ahman B.Livshits B.J.Corcoran K.Maillard S.Z.Béguelin T.Ball P.d.Halleux N.Guts M.Hicks G.Ammons J.Choi M.Gupta N.Giannarakis C.Hawblitzel G.Martínez J.Protzenko P.Vekris J.Weinberger C.Schlesinger G.Barthe B.Grégoire P.Dagand J.Yang Aymeric Fromherz B.Parno G.D.Plotkin C.Keller Antoine Delignat-Lavaud Simon Forest Markulf Kohlweiss Jean Karim Zinzindohoue V.Dumitrescu M.Narasimhamurthy Z.Paraskevopoulou C.Pit-Claudel T.Ramananandro

Talks about:

type (7) secur (4) monad (4) program (3) verifi (3) enforc (3) applic (3) javascript (2) dijkstra (2) gradual (2)

Person: Nikhil Swamy

DBLP: Swamy:Nikhil

Contributed to:

2015

2014

2013

2012

2011

2010

2009

2004

2019

2016

2017

2018

2019

Wrote 19 papers:

POPL-2015-RastogiSFBV #performance #type system #typescript: Safe & Efficient Gradual Typing for TypeScript (AR, NS, CF, GMB, PV), pp. 167–180.
POPL-2014-BartheFGSSB #encryption #implementation #probability #relational #verification: Probabilistic relational verification for cryptographic implementations (GB, CF, BG, PYS, NS, SZB), pp. 193–206.
POPL-2014-SwamyFRBCSB #embedded #javascript #type system: Gradual typing embedded securely in JavaScript (NS, CF, AR, KB, JC, PYS, GMB), pp. 425–438.
PASTE-2013-BallHSL #interactive #web: Increasing human-tool interaction via the web (TB, PdH, NS, DL), pp. 49–52.
PLDI-2013-SwamyWSCL #higher-order #monad #source code #verification: Verifying higher-order programs with the dijkstra monad (NS, JW, CS, JC, BL), pp. 387–398.
POPL-2013-FournetSCDSL #compilation #javascript: Fully abstract compilation to JavaScript (CF, NS, JC, PÉD, PYS, BL), pp. 371–384.
POPL-2012-StrubSFC #coq #named #self: Self-certification: bootstrapping certified typecheckers in F* with Coq (PYS, NS, CF, JC), pp. 571–584.
ICFP-2011-SwamyCFSBY #dependent type #distributed #programming: Secure distributed programming with value-dependent types (NS, JC, CF, PYS, KB, JY), pp. 266–278.
ICFP-2011-SwamyGLH #lightweight #ml #monad #programming: Lightweight monadic programming in ML (NS, NG, DL, MH), pp. 15–27.
ESOP-2010-SwamyCC #data flow #policy: Enforcing Stateful Authorization and Information Flow Policies in Fine (NS, JC, RC), pp. 529–549.
PLDI-2010-ChenCS #compilation #security #verification: Type-preserving compilation of end-to-end verification of security enforcement (JC, RC, NS), pp. 412–423.
ICFP-2009-SwamyHB #formal method: A theory of typed coercions and its applications (NS, MWH, GMB), pp. 329–340.
SIGMOD-2009-CorcoranSH #security #web: Cross-tier, label-based security enforcement for web applications (BJC, NS, MWH), pp. 269–282.
ECOOP-2004-AmmonsCGS #performance #scalability: Finding and Removing Performance Bottlenecks in Large Systems (GA, JDC, MG, NS), pp. 170–194.
ESOP-2019-MartinezADGHHNP #automation #metaprogramming #proving #smt: Meta-F* : Proof Automation with SMT, Tactics, and Metaprograms (GM, DA, VD, NG, CH, CH, MN, ZP, CPC, JP, TR, AR, NS), pp. 30–59.
POPL-2016-SwamyHKRDFBFSKZ #dependent type #multi: Dependent types and multi-monadic effects in F (NS, CH, CK, AR, ADL, SF, KB, CF, PYS, MK, JKZ, SZB), pp. 256–270.
POPL-2017-AhmanHMMPPRS #for free #monad: Dijkstra monads for free (DA, CH, KM, GM, GDP, JP, AR, NS), pp. 515–529.
POPL-2018-AhmanFHMRS: Recalling a witness: foundations and applications of monotonic state (DA, CF, CH, KM, AR, NS), p. 30.
POPL-2019-FromherzGHPRS #assembly #performance: A verified, efficient embedding of a verifiable assembly language (AF, NG, CH, BP, AR, NS), p. 30.