Compiler verification meets cross-language linking via data abstraction. - Peng Wang 048; Santiago Cuéllar; Adam Chlipala (OOPSLA, 2014)

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)

The End of History? Using a Proof Assistant to Replace Language Design with Library Design. - Adam Chlipala; Benjamin Delaware; Samuel Duchovni; Jason Gross; Clément Pit-Claudel; Sorawit Suriyakarn; Peng Wang 048; Katherine Ye (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)

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)

TiML: a functional language for practical complexity analysis with invariants. - Peng Wang 048; Di Wang 017; Adam Chlipala (Proc. ACM Program. Lang., 2017)

Type system for resource bounds with type-preserving compilation. - Peng Wang 048 (2019)

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. - Clément Pit-Claudel; Peng Wang 048; Benjamin Delaware; Jason Gross; Adam Chlipala (IJCAR (2), 2020)