Homotopy Type Theory in Game Semantics

This project falls within the EPSRC research areas "Programming Languages and
Compilers" and "Theoretical Computer Science".

Recent years have seen the development of a new formal language, Homotopy Type
Theory (HoTT), which builds a bridge between abstract mathematics, algebraic
topology to be precise, and research in programming languages, more specifically
dependent type theory. This bridge does not only fortify the project of
formalizing mathematical proofs in a way such that they can be checked by a
computer, it also allows for devising more expressive programming languages.
Software in business and public organisations is used for ever more tasks and is
becoming increasingly complex. In order to depict this complexity while still
providing a maintainable code base, more abstractions in programming languages
are necessary. Meaningful mathematical abstractions can furthermore be used to
prove the correctness of software and thereby ensure the security of our
informational infrastructure. Thus, the applications of foundational research on
HoTT are manifold.

Since HoTT is a relatively new development, it has yet to be fully understood.
In particular, HoTT offers an intricate treatment of identity between
mathematical objects. So far, the properties of identity in HoTT could only be
made sense of from a geometric point of view, but the fact that HoTT can be
applied so fruitfully suggests that this treatment of identity is actually
independent of geometry. One aim of the proposed project is to establish that
the way identity is treated in HoTT is in fact foundational and can be applied
in many areas. This might also resolve some issues regarding the computational
character of HoTT, as some new features break properties of the system that are
desirable when viewing HoTT as a programming language.

We want to apply various mathematical methods in the investigation of HoTT. In
particular, game semantics offers a fine-grained model of programming languages,
we hope to gain new insight HoTT by modelling it in game semantics. We will
connect to previous work that has modelled dependent type theory in game
semantics and try extend it to concepts that are novel to HoTT. More generally
we want to use categorical methods for our purposes and will try to look for
inspiration in other fields such as Quantum logic.

The work will take place in the Quantum group at Oxford's Department of Computer
Science, where many other researchers work on related topics. In the course of
the project, links to other universities might evolve, such as the Carnegie
Mellon University in the USA and Stockholm University in Sweden.