coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Last call: DeepSpec Summer School, July 13-28, 2017

From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
To: types-announce AT lists.seas.upenn.edu, coq-club AT inria.fr, csf-attendees AT mail-infsec.cs.uni-saarland.de, deepspec AT lists.cs.princeton.edu
Subject: [Coq-Club] Last call: DeepSpec Summer School, July 13-28, 2017
Date: Tue, 6 Jun 2017 07:18:50 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT cis.upenn.edu; spf=None smtp.helo=postmaster AT fox.seas.upenn.edu
Ironport-phdr: 9a23:Vh5zNRQFDDFoRZQTNr6gK++crNpsv+yvbD5Q0YIujvd0So/mwa6zZhGN2/xhgRfzUJnB7Loc0qyN4v+mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbF/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHLhcN/kaxVoxyvqQJ4zYPPeo6ZKP9+c7ndfd8GW2ZMWNtaWSxbAoO7aosCF+QNMPtGoIn7pVsBtx6+BQiqBOjy1DJEnGL907c70+s/CwHJwBIvE9wTu3nTt9r6KL8SUeGrw6nS0TrMcehb1iv86IjTaBwhvOmMUqx2ccrX00UgCR7KjkiJpIHjIjib2OMNs22B4OphU+Kik3MopB9vrTi33ccskpfGiZ4PxlDD7yV5z545JcCgSEFlZ96kFoFcuD+HOItrRM4pXmJmuD4ix7EbuZO2fzIGxIkpyhLDcfCKcZWE7gj+WOqPJTp0nHZodbOlixqs70StyPfwWtS73VtOtCZIkNrBu3YQ3BLJ8MeHUOFy/kK51DaPyQ/T7uZELFg6larcJJ8t2KUwmYQJvkTYBCP2hV32g7GQdkUi4OSn9fnoYqj+qp+dMY97lB3+P7wzlsG/Auk0KBUCUmaH9eim1rDv4Ff1TKhUgvAyiqXZtYrVJcUfpq63GQ9V1YMj5g6kADi6yNQYnGcILEhZdx2ZlIXmJ1DOIOviAfeim1SjjjFrx/bcMrL/H5rNM2DPkK39crZl905c1A0zwMhD6JJTE7ENOe78WkvstNPDFRI5KAy1w+P/CNpnzI8eWGSPArWYMKzIq1OI6PgvcKGwY9oJqS7wML0s4fjpkHkylHcZfLK1xt0MZXmjWOl+LkOfJ3fgn5NJGmAT+wE6UebCiVuYUDcVaWz2F6kn6HQyFJ6rC4vOS5uFhbWA2GK6GJNNa2sAAUvKDHHpMp6NUu0IYSSeZMNs1nQIWLW5UJcs3jmqtRTm0PxsNazM4Cwevp//094z6uHOxj8o8jkhRe6Q1WOESmBy1khODwc30bp0rAY1nl2Iyal1mfdVPddS/LVUSgo8M9jRw/EsWIO6YR7IYtrcEAXued6hGzxkFt8=

The first DeepSpec Summer School on Verified Systems will be held in Philadelphia from July 17 to 28, 2017, preceded by an introductory Coq Intensive from July 13 to 15.

The second week is currently full, but there are a few places left for self-funded participants in the first week (Leroy, Pierce, Weirich, and Zdancewic) and the preceding Coq Intensive.

The deadline for registration and hotel booking is next Monday, June 12th.

Overview

Can critical systems be built with no bugs in hardware, operating systems, compilers, crypto, or other key components? It may seem a pipe dream, but the past decade has seen explosive advances in the technology required to realize it. This summer school aims to give participants a wide-ranging overview of several ambitious projects currently underway in this space.

Participants will complete the summer school with a thorough understanding of the conceptual underpinnings of these projects plus considerable hands-on experience with state-of-the-art tools for building verified systems.

Dates

The summer school will open with a three-day intensive course on Coq fundamentals, for participants who are new to Coq. The main lectures take place during the weeks of July 17 and 24.

July 13-15 (Thu-Sat)	Coq intensive
July 17-21	Week 1
July 24-28	Week 2

Lecturers and Topics

Andrew Appel	Verified functional algorithms
Adam Chlipala	Program-specific proof automation
Frans Kaashoek & Nickolai Zeldovich	Certifying software with crashes
Xavier Leroy	The structure of a verified compiler
Benjamin Pierce	Property-based random testing with QuickChick
Zhong Shao	CertiKOS: Certified kit operating systems
Stephanie Weirich	Language specification and variable binding
Steve Zdancewic	Vellvm: Verifying the LLVM

Prerequisites

The DeepSpec summer school is aimed at a wide range of participants, including graduate students, academics, and industrial engineers and researchers.

The Coq proof assistant will serve as a lingua franca for all the lectures. Participants who are not already familiar with Coq at the level of Software Foundations should plan on attending the Coq Intensive before the summer school.

Details

Please see https://deepspec.org/event/dsss17/announcement.html for further information and a link to the registration form.

[Coq-Club] Last call: DeepSpec Summer School, July 13-28, 2017, Benjamin C. Pierce, 06/06/2017