Yannis Juglaret, Cătălin Hritcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. In 29th IEEE Symposium on Computer Security Foundations (CSF). IEEE Computer Society Press, July 2016. arXiv:1602.04503. [ bib | http ]

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 | http ]

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 ]

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, 2016. Version 4.0. http://www.cis.upenn.edu/ bcpierce/sf. [ bib | japanese translation | book ]

Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C Pierce. Programming language techniques for differential privacy. ACM SIGLOG News, 3(1):34-53, January 2016. [ bib | .pdf ]

Benjamin C. Pierce. A Deep Specification for Dropbox, November 2015. Keynote address at Clojure/conj. [ bib | video | slides ]

Benjamin C. Pierce. The Age of Deep Specification, May 2015. Honorary doctorate address at Chalmers University. [ bib | slides ]

Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. Micro-Policies: Formally Verified, Tag-Based Security Monitors. In 36th IEEE Symposium on Security and Privacy (Oakland S&P). IEEE, May 2015. [ bib | short version | slides ]

Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner. Symmetric Lenses. Journal of the ACM, 2015. To appear; extended abstract in POPL 2011. [ bib | short version ]

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 ]

Udit Dhawan, Cătălin Hritcu, Rafi Rubin, Nikos Vasilakis, Silviu Chiricescu, Jonathan M. Smith, Thomas F. Knight, Jr., Benjamin C. Pierce, and André DeHon. Architectural Support for Software-Defined Metadata Processing, 2015. [ bib | .html ]

Benjamin C. Pierce. Micro-Policies: A Framework for Tag-Based Security Monitors, December 2014. Distinguished Lecture at University of Minnesota. [ bib | slides ]

Benjamin C. Pierce. Mysteries of Dropbox, November 2014. Keynote address at CERN Workshop on Cloud Services for File Synchronisation and Sharing. [ bib | video | slides ]

Benjamin C. Pierce. Programmable Hardware Support for Ubiquitous Micro-Policy Enforcement, May 2014. Talk at High-Confidence Software Systems. [ bib | slides ]

Benjamin C. Pierce. Interview with Luke Muehlhauser on Clean-Slate Security Architectures for Machine Intelligence Research Institute blog, May 2014. [ bib | transcript ]

Udit Dhawan, Nikos Vasilakis, Raphael Rubin, Silviu Chiricescu, Jonathan M. Smith, Thomas F. Knight, Benjamin C. Pierce, and André DeHon. PUMP - A Programmable Unit for Metadata Processing. In Proceedings of the 3rd International Workshop on Hardware and Architectural Support for Security and Privacy, HASP '14, New York, NY, USA, 2014. ACM. [ bib | DOI | DOI | http ]

Justin Hsu, Marco Gaboardi, Andreas Haeberlen, Sanjeev Khanna, Arjun Narayan, Benjamin C. Pierce, and Aaron Roth. Differential Privacy: An Economic Method for Choosing Epsilon. In Computer Security Foundations Symposium (CSF), 2014. [ bib | .pdf ]

Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. A Verified Information-Flow Architecture. In Proceedings of the 41st Symposium on Principles of Programming Languages, POPL, January 2014. Full version to appear in Journal of Computer Security, Special Issue on Verified Information Flow Security, 2016. [ bib | full version | .pdf ]

Benjamin C. Pierce. Principles, Meet Practice: An Early Retrospective on SAFE, January 2014. Talk at Principles in Practice Workshop (PiP). [ bib | slides ]

Daniel Wagner. Symmetric Edit Lenses: A New Foundation for Bidirectional Languages. PhD thesis, University of Pennsylvania, 2014. [ bib | .pdf ]

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 | .html ]