<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif;"><div><div style="font-family: Consolas; font-size: medium;">Homotopy Type Theory: Programming and Verification</div><div style="font-family: Consolas; font-size: medium;">2 PostDocs, each 4 Years</div><div style="font-family: Consolas; font-size: medium;">Universities of Strathclyde and Nottingham</div><div style="font-family: Consolas; font-size: medium;"><br></div><div style="font-family: Consolas; font-size: medium;">Applications are invited for two postdocs and one PhD student to work on</div><div style="font-family: Consolas; font-size: medium;">the recently funded EPSRC grant "Homotopy Type Theory: Programming and</div><div style="font-family: Consolas; font-size: medium;">Verification" obtained by Professor Neil Ghani and Dr Conor McBride</div><div style="font-family: Consolas; font-size: medium;">(University of Strathclyde), Dr Thorsten Altenkirch (University of</div><div style="font-family: Consolas; font-size: medium;">Nottingham) and Dr Nicola Gambino (University of Leeds). One postdoc and</div><div style="font-family: Consolas; font-size: medium;">will work on more theoretical aspects of the project in</div><div style="font-family: Consolas; font-size: medium;">Nottingham, while the other postdoc will work on implementation issues in</div><div style="font-family: Consolas; font-size: medium;">Strathclyde. Nevertheless, the reality is that we will be working as a</div><div style="font-family: Consolas; font-size: medium;">team with frequent visits expected between ourselves and our collaborators.</div><div style="font-family: Consolas; font-size: medium;"><br></div><div style="font-family: Consolas; font-size: medium;">Homotopy Type Theory (HoTT) is a revolutionary new approach to type</div><div style="font-family: Consolas; font-size: medium;">theory where types are interpreted as spaces, terms as points and</div><div style="font-family: Consolas; font-size: medium;">equalities as paths. Decades of research in homotopy theory has uncovered</div><div style="font-family: Consolas; font-size: medium;">the structure of such paths and HoTT uses this structure as the basis of</div><div style="font-family: Consolas; font-size: medium;">a new theory of equality. Excitingly, within homotopy theory, one</div><div style="font-family: Consolas; font-size: medium;">naturally studies higher homotopies of paths between paths and this gives</div><div style="font-family: Consolas; font-size: medium;">the higher dimensional structure of equality we previously lacked. The</div><div style="font-family: Consolas; font-size: medium;">objective of this grant is to translate the advances of HoTT into more</div><div style="font-family: Consolas; font-size: medium;">concrete programming language and verification tools.</div><div style="font-family: Consolas; font-size: medium;"><br></div><div style="font-family: Consolas; font-size: medium;">For more details, please email</div><div style="font-family: Consolas; font-size: medium;"><br></div><div style="font-family: Consolas; font-size: medium;">Neil Ghani (<a href="mailto:ng@cis.strath.ac.uk">ng@cis.strath.ac.uk</a>)</div><div style="font-family: Consolas; font-size: medium;">Conor McBride (<a href="mailto:conor.mcbride@strath.ac.uk">conor.mcbride@strath.ac.uk</a>)</div><div style="font-family: Consolas; font-size: medium;">Thorsten Altenkirch (<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>)</div><div style="font-family: Consolas; font-size: medium;">Nicola Gambino (<a href="mailto:n.gambino@leeds.ac.uk">n.gambino@leeds.ac.uk</a>)</div></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 send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.
This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
</PRE></body></html>