Theorems for free for free: parametricity, with and without types. - Amal Ahmed 001; Dustin Jamner; Jeremy G. Siek; Philip Wadler (Proc. ACM Program. Lang., 2017)

Using Binary Analysis Frameworks: The Case for BAP and angr. - Chris Casinghino; J. T. Paasch; Cody Roux; John Altidor; Michael Dixon; Dustin Jamner (NFM, 2019)

Graduality and parametricity: together again for the first time. - Max S. New; Dustin Jamner; Amal Ahmed 001 (Proc. ACM Program. Lang., 2020)

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)

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)

Pyrosome: Verified Compilation for Modular Metatheory. - Dustin Jamner; Gabriel Kammer; Ritam Nag; Adam Chlipala (CoRR, 2025)