<html>
<head>
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space;
-webkit-line-break: after-white-space;" class="" bgcolor="#FFFFFF"
text="#000000">
<span style="color: rgb(51, 51, 51); font-family: 'Helvetica Neue',
Helvetica, Arial, sans-serif; font-size: 17px;" class="">Hello
HACSers,<br>
<br>
At the last workshop, some of you expressed interest in learning
more about the Coq theorem prover. To that end, the following
summer school may be of interest. Please feel free to contact me
personally if you have any questions about it.<br>
<br>
<br>
The first </span><i class="" style="color: rgb(51, 51, 51);
font-family: 'Helvetica Neue', Helvetica, Arial, sans-serif;
font-size: 17px; box-sizing: border-box;"><span class=""
style="box-sizing: border-box; font-weight: 700;">DeepSpec
Summer School on Verified Systems</span></i><span style="color:
rgb(51, 51, 51); font-family: 'Helvetica Neue', Helvetica, Arial,
sans-serif; font-size: 17px;" class=""> will be held in
Philadelphia from July 17 to 28, 2017, preceded by an
introductory </span><i class="" style="color: rgb(51, 51, 51);
font-family: 'Helvetica Neue', Helvetica, Arial, sans-serif;
font-size: 17px; box-sizing: border-box;"><span class=""
style="box-sizing: border-box; font-weight: 700;">Coq Intensive</span></i><span
style="color: rgb(51, 51, 51); font-family: 'Helvetica Neue',
Helvetica, Arial, sans-serif; font-size: 17px;" class=""> from
July 13 to 15. Applications are now open:</span><br class="">
<div bgcolor="#FFFFFF" text="#000000" style="word-wrap: break-word;
-webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"
class="">
<div class="">
<div class=""> <a
href="http://deepspec.org/events/ss17detail.html" class=""
style="font-family: 'Helvetica Neue', Helvetica, Arial,
sans-serif; font-size: 17px;">http://deepspec.org/events/ss17detail.html</a></div>
<h4 class="" style="box-sizing: border-box; font-family:
'Helvetica Neue', Helvetica, Arial, sans-serif; font-weight:
500; line-height: 1.1; color: rgb(51, 51, 51); margin-top:
10px; margin-bottom: 10px; font-size: 21px;">Overview</h4>
<p class="" style="box-sizing: border-box; margin: 0px 0px 10px;
color: rgb(51, 51, 51); font-family: 'Helvetica Neue',
Helvetica, Arial, sans-serif; font-size: 17px;"> Can critical
systems be built with <i class="" style="box-sizing:
border-box;">no bugs</i> in hardware, operating systems,
compilers, crypto, and other key components? It may seem a
pipe dream, but the past decade has seen remarkable advances
in the technology required to realize it.</p>
<p class="" style="box-sizing: border-box; margin: 0px 0px 10px;
color: rgb(51, 51, 51); font-family: 'Helvetica Neue',
Helvetica, Arial, sans-serif; font-size: 17px;"> This summer
school aims to give participants a wide-ranging overview of
several ambitious projects currently underway in this space.
Participants will gain a thorough understanding of the
conceptual underpinnings of these projects plus considerable
hands-on experience with the state-of-the-art tools being used
to build them.</p>
<h4 class="" style="box-sizing: border-box; font-family:
'Helvetica Neue', Helvetica, Arial, sans-serif; font-weight:
500; line-height: 1.1; color: rgb(51, 51, 51); margin-top:
10px; margin-bottom: 10px; font-size: 21px;"> Dates</h4>
<p class="" style="box-sizing: border-box; margin: 0px 0px 10px;
color: rgb(51, 51, 51); font-family: 'Helvetica Neue',
Helvetica, Arial, sans-serif; font-size: 17px;"> The summer
school will open with a three-day intensive course on the
fundamentals of the Coq proof assistant, for participants who
are new to Coq. The main lectures take place during the weeks
of July 17 and 24. </p>
<h4 class="" style="box-sizing: border-box; font-family:
'Helvetica Neue', Helvetica, Arial, sans-serif; font-weight:
500; line-height: 1.1; color: rgb(51, 51, 51); margin-top:
10px; margin-bottom: 10px; font-size: 21px;"> Lecturers and
Topics</h4>
<div class="" style="box-sizing: border-box; margin: 0px 0px
10px; color: rgb(51, 51, 51); font-family: 'Helvetica Neue',
Helvetica, Arial, sans-serif; font-size: 17px;">
<table class="" style="box-sizing: border-box; border-spacing:
0px; border-collapse: collapse; background-color: rgb(255,
255, 224); border: 1px solid black; width: 648px; padding:
15px; color: rgb(51, 51, 51); font-size: 17px;">
<tbody class="" style="box-sizing: border-box;">
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Andrew Appel </td>
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Verified functional
algorithms </td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Adam Chlipala </td>
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Program-specific proof
automation</td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Frans Kaashoek &
Nickolai Zeldovich </td>
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Certifying software
with crashes </td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray; width:
291.23748779296875px;"> Xavier Leroy </td>
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> The structure of a
verified compiler</td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Benjamin Pierce </td>
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Property-based random
testing with QuickChick </td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Zhong Shao </td>
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> CertiKOS: Certified kit
operating systems</td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Stephanie Weirich </td>
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Language specification
and variable binding</td>
</tr>
<tr class="" style="box-sizing: border-box;">
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Steve Zdancewic </td>
<td class="" style="box-sizing: border-box; padding:
5px; border: 1px solid gray;"> Vellvm: Verifying the
LLVM </td>
</tr>
</tbody>
</table>
</div>
<h4 class="" style="box-sizing: border-box; font-family:
'Helvetica Neue', Helvetica, Arial, sans-serif; font-weight:
500; line-height: 1.1; color: rgb(51, 51, 51); margin-top:
10px; margin-bottom: 10px; font-size: 21px;"> More information</h4>
</div>
<div class=""><span class="" style="color: rgb(51, 51, 51);
font-family: 'Helvetica Neue', Helvetica, Arial, sans-serif;
font-size: 17px; background-color: rgb(255, 255, 255);">To
apply, or for more information, please visit</span><span
class="" style="color: rgb(51, 51, 51); font-family:
'Helvetica Neue', Helvetica, Arial, sans-serif; font-size:
17px; background-color: rgb(255, 255, 255);"> </span><font
class="" face="Helvetica Neue,Helvetica,Arial,sans-serif"><span
class="" style="font-size: 17px;"><a
href="http://deepspec.org/events/ss17detail.html" class="">http://deepspec.org/events/ss17detail.html</a></span></font>.</div>
<div class=""><span class="" style="color: rgb(51, 51, 51);
font-family: 'Helvetica Neue', Helvetica, Arial, sans-serif;
font-size: 17px; background-color: rgb(255, 255, 255);"><br
class="">
</span></div>
<div class=""><span class="" style="color: rgb(51, 51, 51);
font-family: 'Helvetica Neue', Helvetica, Arial, sans-serif;
font-size: 17px; background-color: rgb(255, 255, 255);">Applications
received by Feb 15 will be given equal consideration;
applications received after Feb 15 will be considered on a
space- and funds-available basis.<br class="">
<font class="" size="-1"><br class="">
</font></span></div>
</div>
</body>
</html>