Papers


2011
[54] Secure Distributed Programming with Value-Dependent Types (, , , , and ), In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, Association for Computing Machinery, . [bibtex] [url] [doi]
2012
[53] Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (, , and ), In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, . [bibtex] [url] [doi]
[52] Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (, , and ), In SIGPLAN Not., Association for Computing Machinery, volume 47, . [bibtex] [url] [doi]
2013
[51] Fully Abstract Compilation to JavaScript (, , , , and ), In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, . [bibtex] [url] [doi]
[50] Verifying Higher-order Programs with the Dijkstra Monad (, , , and ), In Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation, . [bibtex] [url]
[49] Fully Abstract Compilation to JavaScript (, , , , and ), In SIGPLAN Not., Association for Computing Machinery, volume 48, . [bibtex] [url] [doi]
2014
[48] Probabilistic Relational Verification for Cryptographic Implementations (, , , , and ), In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, . [bibtex] [url] [doi]
[47] Gradual Typing Embedded Securely in JavaScript (, , , , , and ), In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, . [bibtex] [url] [doi]
[46] Gradual Typing Embedded Securely in JavaScript (, , , , , and ), In SIGPLAN Not., Association for Computing Machinery, volume 49, . [bibtex] [url] [doi]
[45] Probabilistic Relational Verification for Cryptographic Implementations (, , , , and ), In SIGPLAN Not., Association for Computing Machinery, volume 49, . [bibtex] [url] [doi]
2016
[44] Dependent Types and Multi-Monadic Effects in F* (, , , , , , , , , and ), In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, . [bibtex] [url]
[43] Towards a Provably Correct Encoding from F* to SMT (), Inria Internship Report, . [bibtex] [pdf]
2017
[42] HACL*: A Verified Modern Cryptographic Library (, , and ), In ACM Conference on Computer and Communications Security, ACM, . [bibtex] [url]
[41]Implementing and Proving the TLS 1.3 Record Layer (, , , , , , , and ), In IEEE Security & Privacy, . [bibtex]
[40]Verified Compilation of Space-Efficient Reversible Circuits (), In Computer Aided Verification (Majumdar, Rupak, Kunčak, Viktor, eds.), Springer International Publishing, . [bibtex]
[39] Dijkstra Monads for Free (, , , , , , and ), In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), ACM, . [bibtex] [url] [doi]
[38] Everest: Towards a Verified, Drop-in Replacement of HTTPS (, , , , , , , , , , , , , , , , , , , , and ), In 2nd Summit on Advances in Programming Languages, . [bibtex] [pdf]
[37] Verified Low-Level Programming Embedded in F* (, , , , , , , , , and ), In PACMPL, volume 1, . [bibtex] [url] [doi]
2018
[36] Recalling a Witness: Foundations and Applications of Monotonic State (, , , , and ), In PACMPL, volume 2, . [bibtex] [url]
[35] A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations (, , , , , , , and ), In The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, . [bibtex] [url]
2019
[34]Everparse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats (, , , , , and ), In Proceedings of the 28th USENIX Conference on Security Symposium, USENIX Association, . [bibtex]
[33] A Verified, Efficient Embedding of a Verifiable Assembly Language (, , , , and ), In PACMPL, . [bibtex] [pdf]
[32] Wys*: A DSL for Verified Secure Multi-party Computations (, and ), In 8th International Conference on Principles of Security and Trust (POST) (Flemming Nielson, David Sands, eds.), Springer, volume 11426, . [bibtex] [url] [doi]
[31] Formally Verified Cryptographic Web Applications in WebAssembly (, , and ), In 2019 IEEE Symposium on Security and Privacy (SP), . [bibtex] [pdf] [doi]
[30] Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms (, , , , , , , , , , , and ), In 28th European Symposium on Programming (ESOP), Springer, . [bibtex] [url] [doi]
[29] The Next 700 Relational Program Logics (, , and ), arXiv:1907.05244, . [bibtex] [url]
[28] Dijkstra Monads for All (, , , , , and ), In 24th ACM SIGPLAN International Conference on Functional Programming (ICFP), . [bibtex] [url]
2020
[27]EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider (, , , , , , , , , , , , , , and ), In 2020 IEEE Symposium on Security and Privacy (SP), . [bibtex] [doi]
[26] HACLxN: Verified Generic SIMD Crypto (for All Your Favourite Platforms) (, , , , , and ), In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, Association for Computing Machinery, . [bibtex] [url] [doi]
[25] Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language (, , , and ), In Proceedings of the Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), . [bibtex] [pdf]
[24] SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs (, , , , and ), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), . [bibtex] [url]
[23] Statically Verified Refinements for Multiparty Protocols (, , , and ), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 4, . [bibtex] [url] [doi]
2021
[22]Verified Functional Programming of an Abstract Interpreter (), In Static Analysis (Dr\uagoi, Cezara, Mukherjee, Suvam, Namjoshi, Kedar, eds.), Springer International Publishing, . [bibtex]
[21] A Tutorial-Style Introduction to $}{\$\backslashtextsf \DY\^\backslashstar $}{\$ (), Chapter in (Dougherty, Daniel, Meseguer, José, Mödersheim, Sebastian Alexander, Rowe, Paul, eds.), Springer International Publishing, . [bibtex] [url] [doi]
[20]Verification of a Merkle Patricia Tree Library Using F (, , , and ), In ArXiv, volume abs/2106.04826, . [bibtex]
[19] An In-Depth Symbolic Security Analysis of the ACME Standard (, , , , , and ), In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, Association for Computing Machinery, . [bibtex] [url] [doi]
[18]$\text{DY}^{\star}$: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code (, , , , , and ), In 2021 IEEE European Symposium on Security and Privacy (EuroS&P), volume , . [bibtex] [doi]
[17]A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer (, , , , , , , and ), In 2021 IEEE Symposium on Security and Privacy (SP), volume , . [bibtex] [doi]
[16] FastVer: Making Data Integrity a Commodity (, , , , , , , , , , , and ), In Proceedings of the 2021 International Conference on Management of Data, Association for Computing Machinery, . [bibtex] [url] [doi]
[15] Programming and Proving with Indexed Effects (, , , and ), . [bibtex] [url]
[14] Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (, , , , , and ), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), . [bibtex] [url]
[13] DICE*: A Formally Verified Implementation of DICE Measured Boot (, , , and ), In 30th Usenix Security Symposium, . [bibtex] [url]
[12] Catala: A Programming Language for the Law (, and ), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 5, . [bibtex] [url] [doi]
2022
[11] Certified Mergeable Replicated Data Types (, , and ), In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, . [bibtex] [url] [doi]
[10]Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (, , and ), In 2022 IEEE Symposium on Security and Privacy (SP), . [bibtex] [doi]
[9] Hardening Attack Surfaces with Formally Proven Binary Format Parsers (, , , , , , , , and ), 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, . [bibtex] [pdf]
[8] Aeneas: Rust Verification by Functional Translation ( and ), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 6, . [bibtex] [url] [doi]
[7] Provably-Safe Multilingual Software Sandboxing using WebAssembly (, and ), In Proceedings of the USENIX Security Symposium, . [bibtex] [pdf]
2023
[6] Comparse: Provably Secure Formats for Cryptographic Protocols (, and ), In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, Association for Computing Machinery, . [bibtex] [url] [doi]
[5] ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER (, , , and ), In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Association for Computing Machinery, . [bibtex] [url] [doi]
[4] TreeSync: Authenticated Group Management for Messaging Layer Security (, , and ), In Proceedings of the 32th USENIX Conference on Security Symposium, USENIX Association, . [bibtex] [url]
[3] FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores (, , , , , , and ), In Certified Programs and Proofs, . [bibtex] [pdf]
[2] Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification (, and ), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 7, . [bibtex] [url] [doi]
[1] Verifying Indistinguishability of Privacy-Preserving Protocols (, and ), In Proc. ACM Program. Lang., Association for Computing Machinery, volume 7, . [bibtex] [url] [doi]