Mechanized Metatheory for the Masses: The PoplMark Challenge. - Brian E. Aydemir; Aaron Bohannon; Matthew Fairbairn; J. Nathan Foster; Benjamin C. Pierce; Peter Sewell; Dimitrios Vytiniotis; Geoffrey Washburn; Stephanie Weirich; Steve Zdancewic (TPHOLs, 2005)

Relational lenses: a language for updatable views. - Aaron Bohannon; Benjamin C. Pierce; Jeffrey A. Vaughan (PODS, 2006)

Nominal Reasoning Techniques in Coq: (Extended Abstract). - Brian E. Aydemir; Aaron Bohannon; Stephanie Weirich (LFMTP@FLoC, 2006)

Boomerang: resourceful lenses for string data. - Aaron Bohannon; J. Nathan Foster; Benjamin C. Pierce; Alexandre Pilkiewicz; Alan Schmitt (POPL, 2008)

Reactive noninterference. - Aaron Bohannon; Benjamin C. Pierce; Vilhelm Sjöberg; Stephanie Weirich; Steve Zdancewic (CCS, 2009)

Sequent calculi and abstract machines. - Zena M. Ariola; Aaron Bohannon; Amr Sabry (ACM Trans. Program. Lang. Syst., 2009)

Featherweight Firefox: Formalizing the Core of a Web Browser. - Aaron Bohannon; Benjamin C. Pierce (WebApps, 2010)