<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Word 14 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman","serif";}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
p
{mso-style-priority:99;
margin:0in;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Times New Roman","serif";}
span.currenthithighlight
{mso-style-name:currenthithighlight;}
span.highlight
{mso-style-name:highlight;}
span.EmailStyle20
{mso-style-type:personal-reply;
font-family:"Calibri","sans-serif";
color:#1F497D;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:2122453458;
mso-list-template-ids:-1512425798;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:\F0B7;
mso-level-tab-stop:.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:"Courier New";
mso-bidi-font-family:"Times New Roman";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:\F0A7;
mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0in;}
ul
{margin-bottom:0in;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-US" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal" style="background:white"><span style="font-family:"Calibri","sans-serif";color:black;background:white">Dear EECS undergrads and grads:<br>
<br>
Companies like Facebook, Twitter, and Jane Street are now using <b>functional languages
</b>(Haskell, Scala, OCaml) to implement critical systems. Why? Because functional programming languages can make it easier to
<b>reason about the programs you write</b>, which often leads to simpler, more maintainable software -- and fewer bugs!<br>
<br>
Taking my 4900/5900 Software Verification course (soon to be renumbered 4201/5201) is a great way to get a jump-start on functional programming (FP), especially if you haven't seen FP before. We'll be spending the first few weeks of the course learning FP in
the incredibly expressive functional programming language Coq. Relevant logistical details:
</span><span style="font-family:"Calibri","sans-serif";color:black"><o:p></o:p></span></p>
<ul style="margin-top:0in" type="disc">
<li class="MsoNormal" style="color:black;mso-list:l0 level1 lfo1;background:white">
<span style="font-family:"Calibri","sans-serif";background:white">M/W lecture 3:05-4pm in ARC 159</span><span style="font-family:"Calibri","sans-serif""><o:p></o:p></span></li><li class="MsoNormal" style="color:black;mso-list:l0 level1 lfo1;background:white">
<span style="font-family:"Calibri","sans-serif";background:white">F lab 3:05-4pm in Stocker 192
</span><span style="font-family:"Calibri","sans-serif""><o:p></o:p></span></li><li class="MsoNormal" style="color:black;mso-list:l0 level1 lfo1;background:white">
<span style="font-family:"Calibri","sans-serif";background:white">Instructor: Gordon Stewart
</span><span style="font-family:"Calibri","sans-serif""><o:p></o:p></span></li><li class="MsoNormal" style="color:black;mso-list:l0 level1 lfo1;background:white">
<span style="font-family:"Calibri","sans-serif";background:white">Last Year's Website, which is representative of the material we'll cover: <a href="http://ace.cs.ohio.edu/~gstewart/courses/5900-16/" id="LPlnk416798">http://ace.cs.ohio.edu/~gstewart/courses/5900-16/</a>
</span><span style="font-family:"Calibri","sans-serif""><o:p></o:p></span></li><li class="MsoNormal" style="color:black;mso-list:l0 level1 lfo1;background:white">
<span style="font-family:"Calibri","sans-serif";background:white">Counts as a <b>
technical elective</b>! </span><span style="font-family:"Calibri","sans-serif""><o:p></o:p></span></li></ul>
<p><span style="font-family:"Calibri","sans-serif";color:black"><o:p> </o:p></span></p>
<div style="margin-bottom:12.0pt">
<p class="MsoNormal" style="background:white"><span style="font-family:"Calibri","sans-serif";color:black;background:white">In later parts of the course, we'll use Coq to
<b>verify </b>both simple functional programs and imperative programs, learning the relevant verification techniques along the way. When I say "verify," I mean we'll use features of the Coq system to prove that our programs are correct -- i.e., they have no
bugs.<br>
<br>
These sorts of verification techniques are useful in high-assurance domains like avionics and cars. Already, companies like Rockwell Collins, Galois (Portland, OR; opening a new office in Dayton), and FireEye are using related methods to build real software
systems -- and industry demand for people who know software verification tools like Coq is only growing.<br>
<br>
So consider taking the course, and I look forward to seeing many of you in the fall!<br>
<br>
Sincerely, <br>
<br>
Gordon Stewart<br>
Asst. Professor, EECS</span><span style="font-family:"Calibri","sans-serif";color:black"><o:p></o:p></span></p>
</div>
<p><span style="font-family:"Calibri","sans-serif";color:black"><o:p> </o:p></span></p>
</div>
</body>
</html>