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

John Hughes, Benjamin C. Pierce, Thomas Arts, and Ulf Norell. Mysteries of Dropbox, October 2015. Under submission. [ bib | short version ]

Yannis Juglaret, Cătălin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components. Technical Report, arXiv:1510.00697, October 2015. [ bib | http ]

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 ]

Silviu Chiricescu, André DeHon, Delphine Demange, Suraj Iyer, Aleksey Kliger, Greg Morrisett, Benjamin C. Pierce, Howard Reubenstein, Jonathan M. Smith, Gregory T. Sullivan, Arun Thomas, Jesse Tov, Christopher M. White, and David Wittenberg. SAFE: A Clean-Slate Architecture for Secure Systems. In Proceedings of the IEEE International Conference on Technologies for Homeland Security, November 2013. [ bib ]

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 to appear in Journal of Functional Programming. [ bib | http ]

Benoît Montagu, Benjamin C. Pierce, and Randy Pollack. A Theory of Information-Flow Labels. In Proceedings of the 2013 IEEE Computer Security Foundations Symposium, June 2013. [ bib | coq code | short version ]

Benjamin C. Pierce. The SAFE Machine: An Architecture for Pervasive Information Flow, June 2013. Invited talk at Computer Security Foundations Symposium (CSF). [ bib | slides ]

Cătălin Hritcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, and Greg Morrisett. All Your IFCException Are Belong To Us. In 34th IEEE Symposium on Security and Privacy (Oakland), May 2013. [ bib | short version ]

Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner. Edit languages for information trees. In Second International Workshop on Bidirectional Transformations (BX), April 2013. [ bib ]

Loris D'Antoni, Marco Gaboardi, Emilio Jesús Gallego Arias, Andreas Haeberlen, and Benjamin Pierce. Sensitivity analysis using type-based constraints. In Proceedings of the 1st annual workshop on Functional programming concepts in domain-specific languages, FPCDSL '13, pages 43-50, New York, NY, USA, 2013. ACM. [ bib | DOI | DOI | http ]

Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear Dependent Types for Differential Privacy. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy, January 2013. [ bib | short version ]