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 (ICST), April 2016. [ bib | short version | slides ]

Yannis Juglaret, Cătălin Hritcu, Arthur Azevedo de Amorim, and Benjamin C. Pierce. Beyond Full Abstraction: Formalizing the Security Guarantees of Low-Level Compartmentalization. Draft, arXiv:1602.04503, February 2016. [ bib | http ]

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 ]

Benjamin C. Pierce, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjoberg, and Brent Yorgey. Software Foundations. Electronic textbook, 2015. bcpierce/sf. [ bib | japanese translation | book ]

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 ]

Cătălin Hritcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, and Dimitrios Vytiniotis. Testing Noninterference, Quickly. arXiv:1409.0393; Submitted to Special Issue of Journal of Functional Programming for ICFP 2013, September 2014. [ bib | http ]

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 under submission to Journal of Computer Security. [ 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 ]