coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Andrew Appel <appel AT CS.Princeton.EDU>
To: coq-club AT inria.fr
Subject: [Coq-Club] The Science of Deep Specification
Date: Thu, 7 Jan 2016 10:20:41 -0500 (EST)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=appel AT CS.Princeton.EDU; spf=Pass smtp.mailfrom=appel AT cs.princeton.edu; spf=None smtp.helo=postmaster AT greenlight.cs.princeton.edu
Ironport-phdr: 9a23:ekrZZhJIaKTxzyMxodmcpTZWNBhigK39O0sv0rFitYgUL/3xwZ3uMQTl6Ol3ixeRBMOAu6wC1LGd7P2ocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0YLojKvtptX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD888784Z8dYmyP+FjDO8QMDNzOGcsocbvqBPrTA2V53JaXH9FvABPBl3s6h3gU4i5mzPiu+41jCCCJcDyZZsPHwy47qFgRQPvjmEqGwNvozKfsdB5kK8O+EHpnBd42YOBJdqY

The U.S. National Science Foundation has just announced this year's three

Expeditions in Computing, their major, high-profile, "flagship" grants; including:

The Science of Deep Specification

Andrew W. Appel, Adam Chlipala, Benjamin Pierce, Zhong Shao, Stephanie Weirich, Steve Zdancewic

(Princeton, Penn, Yale, MIT)

This 5-year "Expedition" will focus on specification and verification of software and hardware in Coq.

We invite you to browse the DeepSpec web site, http://deepspec.org

to learn more of our plans.

We invite participation from the community of researchers

interested in software specification and functional-correctness verification,

both in the U.S. and around the world, both in academia and industry.

We will be looking for postdocs and PhD students, and visitors.

Andrew W. Appel

Princeton University

[Coq-Club] The Science of Deep Specification, Andrew Appel, 01/07/2016
- Re: [Coq-Club] The Science of Deep Specification, Maxime Dénès, 01/07/2016
- Re: [Coq-Club] The Science of Deep Specification, Kevin Sullivan, 01/07/2016