Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations. Electronic textbook, 2017. Version 5.0. http://www.cis.upenn.edu/ bcpierce/sf. [ bib | japanese translation | book ]

Benjamin C. Pierce. Proof Assistant as Teaching Assistant: A View from the Trenches, July 2010. Keynote address at International Conference on Interactive Theorem Proving (ITP). [ bib | slides ]

Benjamin C. Pierce. Lambda, The Ultimate TA: Using a Proof Assistant to Teach Programming Language Foundations, September 2009. Keynote address at International Conference on Functional Programming (ICFP). [ bib | slides ]

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 ]