Benjamin C. Pierce. Using a Proof Assistant to Teach Programming Language Foundations, or, Lambda, the Ultimate TA, April 2008. White paper. [ bib | short version ]

Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 3-15. ACM, January 2008. [ bib | short version ]

Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering Formal Metatheory, July 2007. Submitted for publication. [ bib | short version ]

Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLmark Challenge. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs), August 2005. [ bib | .ps | .pdf ]