2017
[5] Vale: Verifying High-Performance Cryptographic Assembly Code (draft) (, , , , , , , , ) In Proceedings of the USENIX Security Symposium (To appear) . [pdf]
[4] Implementing and Proving the TLS 1.3 Record Layer (, , , , , , , , , ) In 38th IEEE Symposium on Security and Privacy, IEEE Computer Society 2017. . [bibtex] [pdf]
[3] Everest: Towards a Verified, Drop-in Replacement of HTTPS (, , , , , , , , , , , , , , , , , , , , , ) In Proceedings of the Summit on Advances in Programming Languages (SNAPL). .
[2] Verified Low-Level Programming Embedded in F* (, , , , , , , , , , ) Submitted . [pdf]
[1] Dijkstra Monads for Free (, , , , , , , ), In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), . [bibtex] [pdf]