Computing Community Consortium Blog

The goal of the Computing Community Consortium (CCC) is to catalyze the computing research community to debate longer range, more audacious research challenges; to build consensus around research visions; to evolve the most promising visions toward clearly defined initiatives; and to work with the funding organizations to move challenges and visions toward funding initiatives. The purpose of this blog is to provide a more immediate, online mechanism for dissemination of visioning concepts and community discussion/debate about them.

NSF WATCH TALK- The Science of Deep Specification

September 14th, 2017 / in Announcements, NSF, Research News / by Helen Wright

The next WATCH talk, called The Science of Deep Specification is Thursday, September 21st, from 12 PM-1 PM EST.

The presenter is Benjamin Pierce, a Henry Salvatori Professor of Computer and Information Science at the University of Pennsylvania and a Fellow of the ACM. His research interests include programming languages, type systems, language-based security, computer-assisted formal verification, differential privacy, and synchronization technologies. He is the author of the widely used graduate textbooks Types and Programming Languages and Software Foundations. He has served as co-Editor in Chief of the Journal of Functional Programming, as Managing Editor for Logical Methods in Computer Science, and as editorial board member of Mathematical Structures in Computer Science, Formal Aspects of Computing, and ACM Transactions on Programming Languages and Systems. He holds a doctorate honoris causa from Chalmers University. He is also the lead designer of the popular Unison file synchronizer.


Abstraction and modularity underlie all successful hardware and software systems: We build complex artifacts by decomposing them into parts that can be understood separately. Rich specifications based on formal logic are little used in industry today, but a practical platform for working with them could significantly reduce the costs of system implementation and evolution. Recently, research in the area has begun to focus on a particularly rich class of specifications, which might be called deep specifications. Deep specifications are rich (describing complex component behaviors in detail); two-sided (connected to both implementations and clients); formal (written in a mathematical notation with clear semantics to support tools such as type checkers, analysis and testing tools, automated or machine-assisted provers, and advanced IDEs); and live (connected directly to the source code of implementations via machine-checkable proofs or property-based random testing).

This talk presents the key features of deep specifications, surveys recent achievements and ongoing efforts in the research community (in particular, in an NSF-supported “Expedition” at Penn, Princeton, Yale, and MIT on formalizing a rich interconnected collection of deep specifications for critical system software components), and argues that the time is ripe for an intensive effort in this area, involving both academia and industry and integrating research, education, and community building. The ultimate goal is to provide rigorously checked proofs about much larger artifacts than are feasible today, based on decomposition of proof effort across components with deep specifications.

The talk will be held in the new National Science Foundation building (Room w2210/w2220) at 2415 Eisenhower Ave. in Alexandria, VA 22314. The new security requirements require that everyone who enters the building have an entry badge.

Therefore, to attend all future WATCH Talks, please email by 5pm the day before the talk with your name and the name of any other attendees in your group.  There will be a badge waiting for you at the Visitor Entrance; you will need to show a government issued ID to receive your badge.

If you would like to watch the talk online, please register for the free webcast here.

NSF WATCH TALK- The Science of Deep Specification