Enforcing Stateful Authorization and Information Flow Policies in Fine. - Nikhil Swamy; Juan Chen 002; Ravi Chugh (ESOP, 2010)

Type-preserving compilation of end-to-end verification of security enforcement. - Juan Chen 002; Ravi Chugh; Nikhil Swamy (PLDI, 2010)

Verifying stateful programs with substructural state and hoare types. - Johannes Borgström; Juan Chen 002; Nikhil Swamy (PLPV, 2011)

Self-certification: bootstrapping certified typecheckers in F* with Coq. - Pierre-Yves Strub; Nikhil Swamy; Cédric Fournet; Juan Chen 002 (POPL, 2012)

dkal ⋆ : Constructing Executable Specifications of Authorization Protocols. - Jean-Baptiste Jeannin; Guido de Caso; Juan Chen 002; Yuri Gurevich; Prasad Naldurg; Nikhil Swamy (ESSoS, 2013)

Verifying higher-order programs with the dijkstra monad. - Nikhil Swamy; Joel Weinberger; Cole Schlesinger; Juan Chen 002; Benjamin Livshits (PLDI, 2013)

Fully abstract compilation to JavaScript. - Cédric Fournet; Nikhil Swamy; Juan Chen 002; Pierre-Évariste Dagand; Pierre-Yves Strub; Benjamin Livshits (POPL, 2013)

Secure distributed programming with value-dependent types. - Nikhil Swamy; Juan Chen 002; Cédric Fournet; Pierre-Yves Strub; Karthikeyan Bhargavan; Jean Yang 001 (J. Funct. Program., 2013)

Gradual typing embedded securely in JavaScript. - Nikhil Swamy; Cédric Fournet; Aseem Rastogi; Karthikeyan Bhargavan; Juan Chen 002; Pierre-Yves Strub; Gavin M. Bierman (POPL, 2014)