Homotopy Type Theory in Game Semantics

点击翻译按钮获取中文摘要

This project falls within the EPSRC research areas "Programming Languages andCompilers" and "Theoretical Computer Science".Recent years have seen the development of a new formal language, Homotopy TypeTheory (HoTT), which builds a bridge between abstract mathematics, algebraictopology to be precise, and research in programming languages, more specificallydependent type theory. This bridge does not only fortify the project offormalizing mathematical proofs in a way such that they can be checked by acomputer, it also allows for devising more expressive programming languages.Software in business and public organisations is used for ever more tasks and isbecoming increasingly complex. In order to depict this complexity while stillproviding a maintainable code base, more abstractions in programming languagesare necessary. Meaningful mathematical abstractions can furthermore be used toprove the correctness of software and thereby ensure the security of ourinformational infrastructure. Thus, the applications of foundational research onHoTT 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 betweenmathematical objects. So far, the properties of identity in HoTT could only bemade sense of from a geometric point of view, but the fact that HoTT can beapplied so fruitfully suggests that this treatment of identity is actuallyindependent of geometry. One aim of the proposed project is to establish thatthe way identity is treated in HoTT is in fact foundational and can be appliedin many areas. This might also resolve some issues regarding the computationalcharacter of HoTT, as some new features break properties of the system that aredesirable when viewing HoTT as a programming language.We want to apply various mathematical methods in the investigation of HoTT. Inparticular, game semantics offers a fine-grained model of programming languages,we hope to gain new insight HoTT by modelling it in game semantics. We willconnect to previous work that has modelled dependent type theory in gamesemantics and try extend it to concepts that are novel to HoTT. More generallywe want to use categorical methods for our purposes and will try to look forinspiration in other fields such as Quantum logic.The work will take place in the Quantum group at Oxford's Department of ComputerScience, where many other researchers work on related topics. In the course ofthe project, links to other universities might evolve, such as the CarnegieMellon University in the USA and Stockholm University in Sweden.