[TYPES/announce] 2 Postdocs in HoTT

[Neil Ghani]

===============================================

Homotopy Type Theory: Programming and  Verification
2 PostDocs, each 4 Years
Universities of Strathclyde and Nottingham

Applications are invited for two postdocs and one PhD student to work on
the recently funded EPSRC grant "Homotopy Type Theory: Programming and
Verification" obtained by Professor Neil Ghani and Dr Conor McBride
(University of Strathclyde), Dr Thorsten Altenkirch (University of
Nottingham) and Dr Nicola Gambino (University of Leeds). One postdoc and
will work on more theoretical aspects of the project in
Nottingham, while the other postdoc will work on implementation issues in
Strathclyde. Nevertheless, the reality is that we will be working as a
team with frequent visits expected between ourselves and our collaborators.

Homotopy Type Theory (HoTT) is a revolutionary new approach to type
theory where types are interpreted as spaces, terms as points and
equalities as paths. Decades of research in homotopy theory has uncovered
the structure of such paths and HoTT uses this structure as the basis of
a new theory of equality. Excitingly, within homotopy theory, one
naturally studies higher homotopies of paths between paths and this gives
the higher dimensional structure of equality we previously lacked. The
objective of this grant is to translate the advances of HoTT into more
concrete programming language and verification tools.

For more details, please email

Neil Ghani (ng at cis.strath.ac.uk<mailto:ng at cis.strath.ac.uk>)
Conor McBride (conor.mcbride at strath.ac.uk<mailto:conor.mcbride at strath.ac.uk>)
Thorsten Altenkirch (Thorsten.Altenkirch at nottingham.ac.uk<mailto:Thorsten.Altenkirch at nottingham.ac.uk>)
Nicola Gambino (n.gambino at leeds.ac.uk<mailto:n.gambino at leeds.ac.uk>)