Finding a better-than-classical quantum AND/OR algorithm using genetic programming. - Lee Spector; Howard Barnum; Herbert J. Bernstein; Nikhil Swamy (CEC, 1999)

RGL Study in a Hybrid Real-time System. - Ken Hennacy; Nikhil Swamy; Don Perlis (Neural Networks and Computational Intelligence, 2003)

Finding and Removing Performance Bottlenecks in Large Systems. - Glenn Ammons; Jong-Deok Choi; Manish Gupta 002; Nikhil Swamy (ECOOP, 2004)

Dynamic inference of polymorphic lock types. - James Rose; Nikhil Swamy; Michael Hicks 001 (Sci. Comput. Program., 2005)

Managing Policy Updates in Security-Typed Languages. - Nikhil Swamy; Michael Hicks 001; Stephen Tse; Steve Zdancewic (CSFW, 2006)

Safe manual memory management in Cyclone. - Nikhil Swamy; Michael W. Hicks; Greg Morrisett; Dan Grossman; Trevor Jim (Sci. Comput. Program., 2006)

Defeating script injection attacks with browser-enforced embedded policies. - Trevor Jim; Nikhil Swamy; Michael Hicks 001 (WWW, 2007)

Verified implementations of the information card federated identity-management protocol. - Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon 001; Nikhil Swamy (AsiaCCS, 2008)

Fable: A Language for Enforcing User-defined Security Policies. - Nikhil Swamy; Brian J. Corcoran; Michael Hicks 001 (SP, 2008)

Verified enforcement of stateful information release policies. - Nikhil Swamy; Michael Hicks 001 (ACM SIGPLAN Notices, 2008)

Language-based Enforcement of User-defined Security Policies (As Applied to Multi-tier Web Programs). - Nikhil Swamy (2008)

A theory of typed coercions and its applications. - Nikhil Swamy; Michael W. Hicks; Gavin M. Bierman (ICFP, 2009)

Cross-tier, label-based security enforcement for web applications. - Brian J. Corcoran; Nikhil Swamy; Michael W. Hicks (SIGMOD Conference, 2009)

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)

Lightweight monadic programming in ML. - Nikhil Swamy; Nataliya Guts; Daan Leijen; Michael Hicks 001 (ICFP, 2011)

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

Verified Security for Browser Extensions. - Arjun Guha; Matthew Fredrikson; Benjamin Livshits; Nikhil Swamy (IEEE Symposium on Security and Privacy, 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)

Increasing human-tool interaction via the web. - Thomas Ball 001; Peli de Halleux; Nikhil Swamy; Daan Leijen (PASTE, 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)

Probabilistic relational verification for cryptographic implementations. - Gilles Barthe; Cédric Fournet; Benjamin Grégoire; Pierre-Yves Strub; Nikhil Swamy; Santiago Zanella-Béguelin (POPL, 2014)

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)

Polymonadic Programming. - Michael Hicks 001; Gavin M. Bierman; Nataliya Guts; Daan Leijen; Nikhil Swamy (MSFP, 2014)

Modular protections against non-control data attacks. - Cole Schlesinger; Karthik Pattabiraman; Nikhil Swamy; David Walker 001; Benjamin G. Zorn (J. Comput. Secur., 2014)

Safe & Efficient Gradual Typing for TypeScript. - Aseem Rastogi; Nikhil Swamy; Cédric Fournet; Gavin M. Bierman; Panagiotis Vekris (POPL, 2015)

Formal Verification of Smart Contracts: Short Paper. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Anitha Gollamudi; Georges Gonthier; Nadim Kobeissi; Natalia Kulatova; Aseem Rastogi; Thomas Sibut-Pinote; Nikhil Swamy; Santiago Zanella-Béguelin (PLAS@CCS, 2016)

Dependent types and multi-monadic effects in F. - Nikhil Swamy; Catalin Hritcu; Chantal Keller; Aseem Rastogi; Antoine Delignat-Lavaud; Simon Forest; Karthikeyan Bhargavan; Cédric Fournet; Pierre-Yves Strub; Markulf Kohlweiss; Jean Karim Zinzindohoue; Santiago Zanella-Béguelin (POPL, 2016)

Dijkstra Monads for Free. - Danel Ahman; Catalin Hritcu; Guido Martínez; Gordon D. Plotkin; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy (CoRR, 2016)

Implementing and Proving the TLS 1.3 Record Layer. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Markulf Kohlweiss; Jianyang Pan; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin; Jean Karim Zinzindohoue (IACR Cryptol. ePrint Arch., 2016)

Dijkstra monads for free. - Danel Ahman; Catalin Hritcu; Kenji Maillard; Guido Martínez; Gordon D. Plotkin; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy (POPL, 2017)

Everest: Towards a Verified, Drop-in Replacement of HTTPS. - Karthikeyan Bhargavan; Barry Bond; Antoine Delignat-Lavaud; Cédric Fournet; Chris Hawblitzel; Catalin Hritcu; Samin Ishtiaq; Markulf Kohlweiss; K. Rustan M. Leino; Jay R. Lorch; Kenji Maillard; Jianyang Pan; et al. (SNAPL, 2017)

Verified Low-Level Programming Embedded in F*. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (CoRR, 2017)

A Monadic Framework for Relational Verification (Functional Pearl). - Niklas Grimm; Kenji Maillard; Cédric Fournet; Catalin Hritcu; Matteo Maffei; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin (CoRR, 2017)

WYS*: A Verified Language Extension for Secure Multi-party Computations. - Aseem Rastogi; Nikhil Swamy; Michael Hicks 001 (CoRR, 2017)

Verified low-level programming embedded in F. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (Proc. ACM Program. Lang., 2017)

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. - Niklas Grimm; Kenji Maillard; Cédric Fournet; Catalin Hritcu; Matteo Maffei; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin (CPP, 2018)

Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier. - Guido Martínez; Danel Ahman; Victor Dumitrescu; Nick Giannarakis; Chris Hawblitzel; Catalin Hritcu; Monal Narasimhamurthy; Zoe Paraskevopoulou; Clément Pit-Claudel; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; et al. (CoRR, 2018)

Recalling a witness: foundations and applications of monotonic state. - Danel Ahman; Cédric Fournet; Catalin Hritcu; Kenji Maillard; Aseem Rastogi; Nikhil Swamy (Proc. ACM Program. Lang., 2018)

Meta-F ^ star : Proof Automation with SMT, Tactics, and Metaprograms. - Guido Martínez; Danel Ahman; Victor Dumitrescu; Nick Giannarakis; Chris Hawblitzel; Catalin Hritcu; Monal Narasimhamurthy; Zoe Paraskevopoulou; Clément Pit-Claudel; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; et al. (ESOP, 2019)

Wys*: A DSL for Verified Secure Multi-party Computations. - Aseem Rastogi; Nikhil Swamy; Michael Hicks 001 (POST, 2019)

EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. - Tahina Ramananandro; Antoine Delignat-Lavaud; Cédric Fournet; Nikhil Swamy; Tej Chajed; Nadim Kobeissi; Jonathan Protzenko (USENIX Security Symposium, 2019)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cédric Fournet; Tahina Ramananandro; Aseem Rastogi; et al. (IACR Cryptol. ePrint Arch., 2019)

A verified, efficient embedding of a verifiable assembly language. - Aymeric Fromherz; Nick Giannarakis; Chris Hawblitzel; Bryan Parno; Aseem Rastogi; Nikhil Swamy (Proc. ACM Program. Lang., 2019)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cédric Fournet; Natalia Kulatova; Tahina Ramananandro; et al. (SP, 2020)

SteelCore: an extensible concurrent separation logic for effectful dependently typed programs. - Nikhil Swamy; Aseem Rastogi; Aymeric Fromherz; Denis Merigoux; Danel Ahman; Guido Martínez (Proc. ACM Program. Lang., 2020)

FastVer: Making Data Integrity a Commodity. - Arvind Arasu; Badrish Chandramouli; Johannes Gehrke; Esha Ghosh; Donald Kossmann; Jonathan Protzenko; Ravi Ramamurthy; Tahina Ramananandro; Aseem Rastogi; Srinath T. V. Setty; Nikhil Swamy; Alexander van Renen; et al. (SIGMOD Conference, 2021)

Steel: proof-oriented programming in a dependently typed concurrent separation logic. - Aymeric Fromherz; Aseem Rastogi; Nikhil Swamy; Sydney Gibson; Guido Martínez; Denis Merigoux; Tahina Ramananandro (Proc. ACM Program. Lang., 2021)

Hardening attack surfaces with formally proven binary format parsers. - Nikhil Swamy; Tahina Ramananandro; Aseem Rastogi; Irina Spiridonova; Haobin Ni; Dmitry Malloy; Juan Vazquez; Michael Tang; Omar Cardona; Arti Gupta (PLDI, 2022)

FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores. - Arvind Arasu; Tahina Ramananandro; Aseem Rastogi; Nikhil Swamy; Aymeric Fromherz; Kesha Hietala; Bryan Parno; Ravi Ramamurthy (CPP, 2023)

ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. - Haobin Ni; Antoine Delignat-Lavaud; Cédric Fournet; Tahina Ramananandro; Nikhil Swamy (CPP, 2023)

Ranking LLM-Generated Loop Invariants for Program Verification. - Saikat Chakraborty; Shuvendu K. Lahiri; Sarah Fakhoury; Akash Lal; Madanlal Musuvathi; Aseem Rastogi; Aditya Senthilnathan; Rahul Sharma 001; Nikhil Swamy (EMNLP (Findings), 2023)

DiffSpec: Differential Testing with LLMs using Natural Language Specifications and Code Artifacts. - Nikitha Rao; Elizabeth Gilbert; Tahina Ramananandro; Nikhil Swamy; Claire Le Goues; Sarah Fakhoury (CoRR, 2024)

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming. - Saikat Chakraborty; Gabriel Ebner; Siddharth Bhat; Sarah Fakhoury; Sakina Fatima; Shuvendu K. Lahiri; Nikhil Swamy (ICSE, 2025)

3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers. - Sarah Fakhoury; Markus Kuppe 001; Shuvendu K. Lahiri; Tahina Ramananandro; Nikhil Swamy (ICSE, 2025)

PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs. - Gabriel Ebner; Guido Martínez; Aseem Rastogi; Thibault Dardinier; Megan Frisella; Tahina Ramananandro; Nikhil Swamy (Proc. ACM Program. Lang., 2025)

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE. - Tahina Ramananandro; Gabriel Ebner; Guido Martínez; Nikhil Swamy (CoRR, 2025)