|
| [76] | USSL: A Universe-Stratified Concurrent Separation Logic for Intrinsic Proofs of Dependently Typed Programs (Anonymous authors). |
|
| [75] | Secure Distributed Programming with Value-Dependent Types (Swamy, Nikhil, Chen, Juan, Fournet, Cédric, Strub, Pierre-Yves, Bhargavan, Karthikeyan and Yang, Jean), In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, Association for Computing Machinery, 2011. |
|
| [74] | Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (Strub, Pierre-Yves, Swamy, Nikhil, Fournet, Cedric and Chen, Juan), In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, 2012. |
| [73] | Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (Strub, Pierre-Yves, Swamy, Nikhil, Fournet, Cedric and Chen, Juan), In SIGPLAN Not., Association for Computing Machinery, volume 47, 2012. |
|
| [72] | Fully Abstract Compilation to JavaScript (Fournet, Cedric, Swamy, Nikhil, Chen, Juan, Dagand, Pierre-Evariste, Strub, Pierre-Yves and Livshits, Benjamin), In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, 2013. |
| [71] | Verifying Higher-order Programs with the Dijkstra Monad (Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen and Benjamin Livshits), In Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation, 2013. |
| [70] | Secure Distributed Programming with Value-Dependent Types (Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan and Jean Yang), In Journal of Functional Programming, volume 23, 2013. |
| [69] | Fully Abstract Compilation to JavaScript (Fournet, Cedric, Swamy, Nikhil, Chen, Juan, Dagand, Pierre-Evariste, Strub, Pierre-Yves and Livshits, Benjamin), In SIGPLAN Not., Association for Computing Machinery, volume 48, 2013. |
|
| [68] | Probabilistic Relational Verification for Cryptographic Implementations (Barthe, Gilles, Fournet, Cédric, Grégoire, Benjamin, Strub, Pierre-Yves, Swamy, Nikhil and Zanella-Béguelin, Santiago), In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, 2014. |
| [67] | Gradual Typing Embedded Securely in JavaScript (Swamy, Nikhil, Fournet, Cedric, Rastogi, Aseem, Bhargavan, Karthikeyan, Chen, Juan, Strub, Pierre-Yves and Bierman, Gavin), In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, 2014. |
| [66] | Gradual Typing Embedded Securely in JavaScript (Swamy, Nikhil, Fournet, Cedric, Rastogi, Aseem, Bhargavan, Karthikeyan, Chen, Juan, Strub, Pierre-Yves and Bierman, Gavin), In SIGPLAN Not., Association for Computing Machinery, volume 49, 2014. |
| [65] | Probabilistic Relational Verification for Cryptographic Implementations (Barthe, Gilles, Fournet, Cédric, Grégoire, Benjamin, Strub, Pierre-Yves, Swamy, Nikhil and Zanella-Béguelin, Santiago), In SIGPLAN Not., Association for Computing Machinery, volume 49, 2014. |
|
| [64] | 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 Zinzindohoué and Santiago Zanella-Béguelin), In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, 2016. |
| [63] | Towards a Provably Correct Encoding from F* to SMT (Alejandro Aguirre), Inria Internship Report, 2016. |
|
| [62] | HACL*: A Verified Modern Cryptographic Library (Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko and Benjamin Beurdouche), In ACM Conference on Computer and Communications Security, ACM, 2017. |
| [61] | 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 and Jean Karim Zinzindohoue), In IEEE Security & Privacy, 2017. |
| [60] | Verified Compilation of Space-Efficient Reversible Circuits (Amy, Matthew, Roetteler, Martin and Svore, Krysta M.), In Computer Aided Verification (Majumdar, Rupak, Kunčak, Viktor, eds.), Springer International Publishing, 2017. |
| [59] | Dijkstra Monads for Free (Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi and Nikhil Swamy), In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), ACM, 2017. |
| [58] | 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, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin and Jean-Karim Zinzindohoué), In 2nd Summit on Advances in Programming Languages, 2017. |
| [57] | Verified Low-Level Programming Embedded in F* (Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet and Nikhil Swamy), In PACMPL, volume 1, 2017. |
|
| [56] | Recalling a Witness: Foundations and Applications of Monotonic State (Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi and Nikhil Swamy), In PACMPL, volume 2, 2018. |
| [55] | 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 and Santiago Zanella-Béguelin), In The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018. |
|
| [54] | Everparse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats (Ramananandro, Tahina, Delignat-Lavaud, Antoine, Fournet, Cédric, Swamy, Nikhil, Chajed, Tej, Kobeissi, Nadim and Protzenko, Jonathan), In Proceedings of the 28th USENIX Conference on Security Symposium, USENIX Association, 2019. |
| [53] | A Verified, Efficient Embedding of a Verifiable Assembly Language (Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi and Nikhil Swamy), In PACMPL, 2019. |
| [52] | Wys*: A DSL for Verified Secure Multi-party Computations (Aseem Rastogi, Nikhil Swamy and Michael Hicks), In 8th International Conference on Principles of Security and Trust (POST) (Flemming Nielson, David Sands, eds.), Springer, volume 11426, 2019. |
| [51] | Formally Verified Cryptographic Web Applications in WebAssembly (J. Protzenko, B. Beurdouche, D. Merigoux and K. Bhargavan), In 2019 IEEE Symposium on Security and Privacy (SP), 2019. |
| [50] | Meta-F*: 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 and Nikhil Swamy), In 28th European Symposium on Programming (ESOP), Springer, 2019. |
| [49] | The Next 700 Relational Program Logics (Kenji Maillard, Catalin Hritcu, Exequiel Rivas and Antoine Van Muylder), arXiv:1907.05244, 2019. |
| [48] | Dijkstra Monads for All (Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas and Éric Tanter), In 24th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2019. |
|
| [47] | EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider (Protzenko, Jonathan, Parno, Bryan, Fromherz, Aymeric, Hawblitzel, Chris, Polubelova, Marina, Bhargavan, Karthikeyan, Beurdouche, Benjamin, Choi, Joonwon, Delignat-Lavaud, Antoine, Fournet, Cédric, Kulatova, Natalia, Ramananandro, Tahina, Rastogi, Aseem, Swamy, Nikhil, Wintersteiger, Christoph M. and Zanella-Beguelin, Santiago), In 2020 IEEE Symposium on Security and Privacy (SP), 2020. |
| [46] | HACLxN: Verified Generic SIMD Crypto (for All Your Favourite Platforms) (Polubelova, Marina, Bhargavan, Karthikeyan, Protzenko, Jonathan, Beurdouche, Benjamin, Fromherz, Aymeric, Kulatova, Natalia and Zanella-Béguelin, Santiago), In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, Association for Computing Machinery, 2020. |
| [45] | Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language (Bosamiya, Jay, Gibson, Sydney, Li, Yao, Parno, Bryan and Hawblitzel, Chris), In Proceedings of the Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2020. |
| [44] | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs (Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman and Guido Martínez), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2020. |
| [43] | Statically Verified Refinements for Multiparty Protocols (Zhou, Fangyi, Ferreira, Francisco, Hu, Raymond, Neykova, Rumyana and Yoshida, Nobuko), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 4, 2020. |
|
| [42] | Verified Functional Programming of an Abstract Interpreter (Franceschino, Lucas, Pichardie, David and Talpin, Jean-Pierre), In Static Analysis (Dr\uagoi, Cezara, Mukherjee, Suvam, Namjoshi, Kedar, eds.), Springer International Publishing, 2021. |
| [41] | A Tutorial-Style Introduction to DY* (Bhargavan, Karthikeyan, Bichhawat, Abhishek, Do, Quoc Huy, Hosseyni, Pedram, Küsters, Ralf, Schmitz, Guido and Würtele, Tim), Chapter in (Dougherty, Daniel, Meseguer, José, Mödersheim, Sebastian Alexander, Rowe, Paul, eds.), Springer International Publishing, 2021. |
| [40] | Verification of a Merkle Patricia Tree Library Using F* (Sota Sato, Ryotaro Banno, Junji Furuse, Kohei Suenaga and Atsushi Igarashi), In ArXiv, volume abs/2106.04826, 2021. |
| [39] | An In-Depth Symbolic Security Analysis of the ACME Standard (Bhargavan, Karthikeyan, Bichhawat, Abhishek, Do, Quoc Huy, Hosseyni, Pedram, Küsters, Ralf, Schmitz, Guido and Würtele, Tim), In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, Association for Computing Machinery, 2021. |
| [38] | DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code (Bhargavan, Karthikeyan, Bichhawat, Abhishek, Do, Quoc Huy, Hosseyni, Pedram, Küsters, Ralf, Schmitz, Guido and Würtele, Tim), In 2021 IEEE European Symposium on Security and Privacy (EuroS&P), volume , 2021. |
| [37] | A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer (Delignat-Lavaud, Antoine, Fournet, Cédric, Parno, Bryan, Protzenko, Jonathan, Ramananandro, Tahina, Bosamiya, Jay, Lallemand, Joseph, Rakotonirina, Itsaka and Zhou, Yi), In 2021 IEEE Symposium on Security and Privacy (SP), volume , 2021. |
| [36] | FastVer: Making Data Integrity a Commodity (Arasu, Arvind, Chandramouli, Badrish, Gehrke, Johannes, Ghosh, Esha, Kossmann, Donald, Protzenko, Jonathan, Ramamurthy, Ravi, Ramananandro, Tahina, Rastogi, Aseem, Setty, Srinath, Swamy, Nikhil, van Renen, Alexander and Xu, Min), In Proceedings of the 2021 International Conference on Management of Data, Association for Computing Machinery, 2021. |
| [35] | Programming and Proving with Indexed Effects (Aseem Rastogi, Guido Martínez, Aymeric Fromherz, Tahina Ramananandro and Nikhil Swamy), Technical report, 2021. |
| [34] | Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux and Tahina Ramananandro), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2021. |
| [33] | DICE*: A Formally Verified Implementation of DICE Measured Boot (Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani and Aditya V. Thakur), In 30th Usenix Security Symposium, 2021. |
| [32] | Catala: A Programming Language for the Law (Merigoux, Denis, Chataing, Nicolas and Protzenko, Jonathan), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 5, 2021. |
|
| [31] | Certified Mergeable Replicated Data Types (Soundarapandian, Vimala, Kamath, Adharsh, Nagar, Kartik and Sivaramakrishnan, KC), In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2022. |
| [30] | Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Ho, Son, Protzenko, Jonathan, Bichhawat, Abhishek and Bhargavan, Karthikeyan), In 2022 IEEE Symposium on Security and Privacy (SP), 2022. |
| [29] | Q*: Implementing Quantum Separation Logic in F* (Kesha Hietala, Sarah Marshall, Robert Rand and Nikhil Swamy), PLanQC 2022 (extended abstract), 2022. |
| [28] | 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 and Arti Gupta), In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI '22), June 13–17, 2022, San Diego, CA, USA, 2022. |
| [27] | Aeneas: Rust Verification by Functional Translation (Ho, Son and Protzenko, Jonathan), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 6, 2022. |
| [26] | Provably-Safe Multilingual Software Sandboxing using WebAssembly (Bosamiya, Jay, Lim, Wen Shih and Parno, Bryan), In Proceedings of the USENIX Security Symposium, 2022. |
|
| [25] | Comparse: Provably Secure Formats for Cryptographic Protocols (Wallez, Théophile, Protzenko, Jonathan and Bhargavan, Karthikeyan), In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, Association for Computing Machinery, 2023. |
| [24] | ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER (Ni, Haobin, Delignat-Lavaud, Antoine, Fournet, Cédric, Ramananandro, Tahina and Swamy, Nikhil), In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Association for Computing Machinery, 2023. |
| [23] | Pipit: Reactive Systems in F* (Extended Abstract) (Amos Robinson and Alex Potanin), TyDe 2023 (extended abstract), 2023. |
| [22] | A Theorem Proving Approach to Programming Language Semantics (Subhajit Roy), In 2023 IEEE/ACM 45th International Conference on Software Engineering: Software Engineering Education and Training (ICSE-SEET), 2023. |
| [21] | TreeSync: Authenticated Group Management for Messaging Layer Security (Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche and Karthikeyan Bhargavan), In Proceedings of the 32th USENIX Conference on Security Symposium, USENIX Association, 2023. |
| [20] | FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores (Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno and Ravi Ramamurthy), In Certified Programs and Proofs, 2023. |
| [19] | Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification (Ho, Son, Fromherz, Aymeric and Protzenko, Jonathan), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 7, 2023. |
| [18] | Verifying Indistinguishability of Privacy-Preserving Protocols (Linvill, Kirby, Kaki, Gowtham and Wustrow, Eric), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 7, 2023. |
|
| [17] | Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems (Amos Robinson and Alex Potanin), In 38th European Conference on Object-Oriented Programming, ECOOP 2024, September 16-20, 2024, Vienna, Austria (Jonathan Aldrich, Guido Salvaneschi, eds.), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, volume 313, 2024. |
| [16] | StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator (Antonin Reitz, Aymeric Fromherz and Jonathan Protzenko), In CoRR, volume abs/2403.09435, 2024. |
| [15] | Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming (Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu K. Lahiri and Nikhil Swamy), In CoRR, volume abs/2405.01787, 2024. |
| [14] | 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers (Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro and Nikhil Swamy), 2024. |
| [13] | Securing Verified IO Programs Against Unverified Code in F* (Andrici, Cezar-Constantin, Ciobâcă, Ștefan, Hri\ctcu, C\uat\ualin, Martínez, Guido, Rivas, Exequiel, Tanter, Éric and Winterhalter, Théo), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 8, 2024. |
|
| [12] | Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust (Karthikeyan Bhargavan, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch and Bas Spitters), In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, 2025. |
| [11] | Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE (Tahina Ramananandro, Gabriel Ebner, Guido Martínez and Nikhil Swamy), In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, 2025. |
| [10] | A Mechanically Verified Garbage Collector for OCaml (Sheera Shamsu, Dipesh Kafle, Dhruv Maroo, Kartik Nagar, Karthikeyan Bhargavan and KC Sivaramakrishnan), In Journal of Automated Reasoning, volume 69, 2025. |
| [9] | PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs (Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro and Nikhil Swamy), In Proceedings of the ACM on Programming Languages, volume 9, 2025. |
| [8] | Automatically Verifying Replication-Aware Linearizability (Vimala Soundarapandian, Kartik Nagar, Aseem Rastogi and KC Sivaramakrishnan), In Proceedings of the ACM on Programming Languages, volume 9, 2025. |
| [7] | SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F* (Andrici, Cezar-Constantin, Ahman, Danel, Hri\ctcu, C\uat\ualin, Icleanu, Ruxandra, Martínez, Guido, Rivas, Exequiel and Winterhalter, Théo), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 9, 2025. |
|
| [6] | DY* Unchained: Now with Composable Security Proofs and Precise Compromise Scenarios (Théophile Wallez), In 2026 IEEE Symposium on Security and Privacy (SP), IEEE, 2026. |
| [5] | Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic (Guido Martínez, Bastian Köpcke, Jonáš Fiala, Gabriel Ebner, Tahina Ramananandro, Michel Steuwer, Tyler Sorensen and Nikhil Swamy), In Proceedings of the ACM on Programming Languages, volume 10, 2026. |
| [4] | Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software (Danel Ahman, Karthikeyan Bhargavan, Barry Bond, Jay Bosamiya, Christopher Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Aymeric Fromherz, Sydney Gibson, Chris Hawblitzel, Cătălin Hrițcu, Markulf Kohlweiss, Guido Martínez, Haobin Ni, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Exequiel Rivas, Nikhil Swamy and Santiago Zanella-Béguelin), In ACM Transactions on Programming Languages and Systems, volume 48, 2026. |
| [3] | Misquoted No More: Securely Extracting F* Programs with IO (Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Cătălin Hrițcu, Exequiel Rivas and Théo Winterhalter), In Proceedings of the ACM on Programming Languages, volume 10, 2026. |
| [2] | Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report) (Eleftherios Ioannidis, Nikhil Swamy, Gabriel Ebner, Matthai Philipose and Tahina Ramananandro), In Proceedings of the ACM on Programming Languages, volume 10, 2026. |
| [1] | The ART of Agentic Proof-Oriented Programming: Audits, Rubrics, and Templates (Nikhil Swamy, Tahina Ramananandro, Guido Martínez, Gabriel Ebner, Shuvendu Lahiri and Lef Ioannidis), 2026. |
