<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=utf-8">
<meta name="Generator" content="Microsoft Word 15 (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:0cm;
margin-bottom:.0001pt;
font-size:12.0pt;
font-family:"Calibri",sans-serif;}
h2
{mso-style-priority:9;
mso-style-link:"Heading 2 Char";
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:18.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:#954F72;
text-decoration:underline;}
span.Heading2Char
{mso-style-name:"Heading 2 Char";
mso-style-priority:9;
mso-style-link:"Heading 2";
font-family:"Calibri",sans-serif;
font-weight:bold;}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
p.zfr3q, li.zfr3q, div.zfr3q
{mso-style-name:zfr3q;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.EmailStyle20
{mso-style-type:personal;
font-family:"Calibri",sans-serif;
color:windowtext;}
span.apple-converted-space
{mso-style-name:apple-converted-space;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:288359526;
mso-list-template-ids:-1276622274;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1
{mso-list-id:1956517686;
mso-list-template-ids:1678007720;}
@list l1:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level2
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></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-GB" link="#0563C1" vlink="#954F72">
<div class="WordSection1">
<p class="MsoNormal"><span class="apple-converted-space"><span style="color:black"> </span></span><span style="color:black"> COST action CA15123 EUTYPES<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"> Summer School on Types for Programming and Verification<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black"> <span class="apple-converted-space"> </span>Ohrid, Macedonia, 30 August – 4 September 2019<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black"> https://sites.google.com/view/2019eutypesschool/home<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"> <o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"> CALL FOR APPLICATIONS<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"> <o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">BACKGROUND<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">Types are pervasive in programming and information technology. A type<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">defines a formal interface between software components, allowing the<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">automatic verification of their connections, and greatly enhancing the<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">robustness and reliability of computations and communications. In rich<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">dependent type theories, the full functional specification of a<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">program can be expressed as a type. Type systems have rapidly evolved<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">over the past years, becoming more sophisticated, capturing new<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">aspects of the behaviour of programs and the dynamics of their<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">execution.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">The aim of this summer school is to provide advanced training,<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">especially to PhD students and early-career researchers, in all<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">aspects of the theory and practice of type theory and applications.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">LECTURERS AND COURSES<o:p></o:p></span></p>
<p class="zfr3q" style="margin-left:0cm;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:#212121"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121">Course 1: Hugo Herbelin: Introduction to lambda calculus & type theory<o:p></o:p></span></p>
<p class="zfr3q" style="margin-left:0cm;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:#212121"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121"><o:p> </o:p></span></p>
<p class="zfr3q" style="margin-left:0cm;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:#212121"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121">Course 2: Jesper Coeckx: Correct-by-construction programming in Agda<o:p></o:p></span></p>
<p class="zfr3q" style="margin-left:0cm;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:#212121"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121"><o:p> </o:p></span></p>
<p class="zfr3q" style="margin-left:0cm;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:#212121"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121">Course 3 : Yves Bertot: Introductory course on Coq/Gallina<o:p></o:p></span></p>
<p class="zfr3q" style="margin-left:0cm;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:#212121"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121"><o:p> </o:p></span></p>
<p class="zfr3q" style="margin-left:0cm;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:#212121"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121">Course 4 : Xavier Leroy: Proving the correctness of a compiler<o:p></o:p></span></p>
<p class="zfr3q" style="margin-left:0cm;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:#212121"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121"><o:p> </o:p></span></p>
<p class="zfr3q" style="margin-left:0cm;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:#212121"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121">Course 5: Nicolai Kraus: Introduction to homotopy type theory
<o:p></o:p></span></p>
<p class="zfr3q" style="mso-margin-top-alt:0cm;margin-right:0cm;margin-bottom:4.5pt;margin-left:0cm;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:#212121"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">APPLICATION<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">The capacity of the summer school is up to 40 students. <o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="zfr3q" style="margin:0cm;margin-bottom:.0001pt;text-indent:-18.0pt;mso-list:l1 level1 lfo4">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:black"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:black;background:white">Accommodation, full board (i.e., including all meals): 5 nights</span><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121">
@ </span><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:black;background:white">€35</span><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121"> =
</span><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:black;background:white">€ 17</span><span style="font-size:11.5pt;font-family:"Arial",sans-serif;color:#212121">5. Extra nights cost also €35.
</span><span style="color:black"><o:p></o:p></span></p>
<p class="zfr3q" style="margin:0cm;margin-bottom:.0001pt;text-indent:-18.0pt;mso-list:l1 level1 lfo4">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Wingdings;color:black"><span style="mso-list:Ignore">§<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">A maximum of 30 students (PhD students / early-career researchers) from countries involved in EUTYPES can receive a grant from the COST action to partially cover their costs.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">To apply for a place in the school and a grant, please fill out (as soon as possible) the form at<span class="apple-converted-space"> </span></span><a href="http://tiny.cc/olbq8y">http://tiny.cc/olbq8y</a><span style="font-size:11.0pt"><o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">Application deadline: 15 July 2019.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">Notification of acceptance and funding: <o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"> continuously, at the latest by 22 July 2019.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">VENUE<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">Ohrid<span class="apple-converted-space"> </span>is a small town on Lake<span class="apple-converted-space"> </span>Ohrid<span class="apple-converted-space"> </span>in Macedonia, southwest of<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">Skopje.<span class="apple-converted-space"> </span>Ohrid<span class="apple-converted-space"> </span>is notable for once having had 365 churches, one for<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">each day of the year, and has been referred to as the Jerusalem of the<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">Balkans.<span class="apple-converted-space"> </span>Ohrid<span class="apple-converted-space"> </span>and Lake<span class="apple-converted-space"> </span>Ohrid<span class="apple-converted-space"> </span>are on UNESCO's
lists of cultural and<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">natural World Heritage sites.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">The school will be held in the Congress Centre of<span class="apple-converted-space"> </span>Ohrid, which is also<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">the accommodation site.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">TRAVEL<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">Most participants will have to fly to Skopje and then get to<span class="apple-converted-space"> </span>Ohrid<span class="apple-converted-space"> </span>by<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">bus.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">WizzAir operates direct flights to<span class="apple-converted-space"> </span>Ohrid<span class="apple-converted-space"> </span>from Basel-Mulhouse-Freiburg<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black">and London Luton.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">ORGANIZERS<o:p></o:p></span></p>
<p class="MsoNormal"><span style="color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="color:black">Thorsten Altenkirch Herman Geuvers, Marija Mihova<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt"><o:p> </o:p></span></p>
</div>
<PRE>
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
</PRE></body>
</html>