2017
[3] Implementing and Proving the TLS 1.3 Record Layer (, , , , , , , , , ) Submitted . [bibtex] [pdf]
[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), . (To appear) [bibtex] [pdf]