Streetscore - Predicting the Perceived Safety of One Million Streetscapes. - Nikhil Naik 003; Jade Philipoom; Ramesh Raskar; César A. Hidalgo 001 (CVPR Workshops, 2014)

Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises. - Andres Erbsen; Jade Philipoom; Jason Gross; Robert Sloan 001; Adam Chlipala (ACM SIGOPS Oper. Syst. Rev., 2020)

Accelerating Verified-Compiler Development with a Verified Rewriting Engine. - Jason Gross; Andres Erbsen; Jade Philipoom; Miraya Poddar-Agrawal; Adam Chlipala (ITP, 2022)

Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. - Clément Pit-Claudel; Jade Philipoom; Dustin Jamner; Andres Erbsen; Adam Chlipala (PLDI, 2022)

Towards ML-KEM & ML-DSA on OpenTitan. - Amin Abdulrahman; Felix Oberhansl; Hoang Nguyen Hien Pham; Jade Philipoom; Peter Schwabe; Tobias Stelzer; Andreas Zankl (IACR Cryptol. ePrint Arch., 2024)

Foundational Integration Verification of a Cryptographic Server. - Andres Erbsen; Jade Philipoom; Dustin Jamner; Ashley Lin; Samuel Gruetter; Clément Pit-Claudel; Adam Chlipala (Proc. ACM Program. Lang., 2024)

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. - Jason Gross; Andres Erbsen; Jade Philipoom; Rajashree Agrawal; Adam Chlipala (J. Autom. Reason., 2024)