Benjamin C. Pierce. Specifying the DeepSpec Web Server, June 2018. Talk at DeepSpec workshop. [ bib | slides ]

Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. Programming Language Foundations. Software Foundations series, volume 2. Electronic textbook, May 2018. Version 5.5. http://www.cis.upenn.edu/ bcpierce/sf. [ bib | japanese translation | book ]

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

Benjamin C. Pierce. The Science of Deep Specification, April 2018. Invited keynote at ETAPS / POST. [ bib | video | slides ]

Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce. Generating good generators for inductive relations. PACMPL, 2(POPL):45:1--45:30, 2018. [ bib | DOI | DOI | short version | pdf ]

Benjamin C. Pierce. The Science of Deep Specification, September 2017. WATCH lecture at NSF. [ bib ]

Arthur Azevedo de Amorim, Cătălin Hritcu, and Benjamin C. Pierce. The Meaning of Memory Safety. arXiv:1705.07354, May 2017. [ bib | pdf ]

Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. Position paper: the science of deep specification. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, 375(2104), 2017. [ bib | DOI | arXiv | DOI | pdf ]

Arthur Azevedo de Amorim, Cătălin Hritcu, and Benjamin C. Pierce. The Meaning of Memory Safety. In ACM Conference on Computer and Communications Security (CCS), 2017. Under submission. [ bib ]

Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hritcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia. Beginner's Luck: A Language for Random Generators. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 2017. [ bib | pdf ]

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. Interview with Markus Völter on The Science of Deep Specification for Omega Tau podcast, November 2016. [ bib | transcript ]

Benjamin C. Pierce. Interview with Tijs van der Storm on The Science of Deep Specification for release.nl magazine, November 2016. [ bib | transcript ]

Benjamin C. Pierce. The Science of Deep Specification, November 2016. Invited keynote at SPLASH / OOPSLA. [ bib | video | slides ]

Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hritcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia. Beginner's Luck: A Language for Random Generators. Draft, arXiv:1607.05443, July 2016. [ bib | pdf ]

Benjamin C. Pierce. The Science of Deep Specification, May 2016. High-Confidence Software Systems (HCSS). [ bib | slides ]

John Hughes, Benjamin C. Pierce, Thomas Arts, and Ulf Norell. Mysteries of Dropbox: Property-Based Testing of a Distributed Synchronization Service. In International Conference on Software Testing, Verification and Validation (ICST), April 2016. [ bib | short version | slides ]

Zoe Paraskevopoulou, Cătălin Hritcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. Foundational Property-Based Testing. In International Conference on Interactive Theorem Proving (ITP), 2015. [ bib ]

Maxime Dénès, Catalin Hritcu, Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce. QuickChick: Property-Based Testing for Coq (abstract). In VSL, 2014. [ bib | pdf ]

Cătălin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, and Leonidas Lampropoulos. Testing Noninterference, Quickly. In 18th ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2013. Full version in Journal of Functional Programming, special issue for ICFP 2013, 26:e4 (62 pages), April 2016. Technical Report available as arXiv:1409.0393. [ bib | pdf ]

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 | pdf | .ps ]