<html>
<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:"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;
font-size:11.0pt;
font-family:"Calibri",sans-serif;
mso-ligatures:standardcontextual;
mso-fareast-language:EN-US;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
mso-fareast-language:EN-US;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></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" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">The Department of Computer Science at the University of Bath has vacancies for academic appointments across its four main research groups:<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><a href="https://urldefense.com/v3/__https://www.bath.ac.uk/campaigns/join-the-department-of-computer-science/__;!!IBzWLUs!S4r7Y4lXGjnqHYV6OjZkxbfR3Cb05weT9H4aI0DgUVM8ttndA2tFlKtVpXiGWzV4r7W29pb8g_dzs4YD1-sPPjXB0GtKuH9G$">https://www.bath.ac.uk/campaigns/join-the-department-of-computer-science/</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">This includes the Mathematical Foundations of Computation group, where we are particularly looking for individuals with research interests in areas around formal mathematics and computer assisted reasoning, including but not limited to:<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">- proof assistants (e.g. Agda, Coq, Isabelle, Lean)<o:p></o:p></p>
<p class="MsoNormal">- certified mathematical libraries<o:p></o:p></p>
<p class="MsoNormal">- logical systems, proof theory and type theory<o:p></o:p></p>
<p class="MsoNormal">- certified programming and program synthesis<o:p></o:p></p>
<p class="MsoNormal">- automated reasoning<o:p></o:p></p>
<p class="MsoNormal">- applications of AI and machine learning to formal mathematics<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">The official job announcement and online application form can be found here:<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><a href="https://urldefense.com/v3/__https://www.bath.ac.uk/jobs/Vacancy.aspx?ref=ED11636__;!!IBzWLUs!S4r7Y4lXGjnqHYV6OjZkxbfR3Cb05weT9H4aI0DgUVM8ttndA2tFlKtVpXiGWzV4r7W29pb8g_dzs4YD1-sPPjXB0LYPt519$">https://www.bath.ac.uk/jobs/Vacancy.aspx?ref=ED11636</a><o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">*Important dates*<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Application deadline: 15 October 2024<o:p></o:p></p>
<p class="MsoNormal">Interviews are planned to take place on the 25, 26, 27 November and 2 and 3 December 2024.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">For any questions about the post or the recruitment process, please contact James Davenport (masjhd AT bath.ac.uk) or Thomas Powell (trjp20 AT bath.ac.uk).<o:p></o:p></p>
</div>
</body>
</html>