Homotopy Type Theory in Game Semantics

本项目福尔斯属于EPSRC的研究领域“程序设计语言与程序设计”和“理论计算机科学”。近年来，一种新的形式化语言--同伦类型理论（HoTT）得到了发展，它在抽象数学、代数拓扑学和程序设计语言研究之间架起了一座桥梁，更确切地说，是依赖类型理论。这座桥梁不仅加强了数学证明的形式化工程，使其能够被计算机检查，它还允许设计出更具表现力的编程语言。商业和公共组织中的软件用于越来越多的任务，并且变得越来越复杂。为了描述这种复杂性，同时仍然提供一个主要的代码库，在编程语言中进行更多的抽象是必要的。有意义的数学抽象还可以用来证明软件的正确性，从而确保我们的信息基础设施的安全性。因此，HoTT的基础研究的应用是多方面的。由于HoTT是一个相对较新的发展，它还没有得到充分的理解。特别是，HoTT提供了一个复杂的处理同一性之间的数学对象。到目前为止，HoTT中的恒等式的性质只能从几何的角度来理解，但HoTT可以如此富有成效地应用的事实表明，这种恒等式的处理实际上是独立于几何的。该项目的一个目标是确定HoTT中对待身份的方式实际上是基础性的，可以应用于许多领域。这也可能解决一些关于HoTT的计算特性的问题，因为一些新的特性打破了将HoTT视为编程语言时所期望的系统特性。特别是，游戏语义提供了一个细粒度的编程语言模型，我们希望通过在游戏语义中对其进行建模来获得新的见解。我们将连接到以前的工作，在博弈论中建模依赖类型理论，并尝试将其扩展到HoTT的新概念。更一般地说，我们希望使用分类方法来实现我们的目的，并将尝试在其他领域（如量子逻辑）中寻找灵感。这项工作将在牛津大学计算机科学系的量子组进行，那里有许多其他研究人员从事相关主题的工作。在这个项目的过程中，可能会发展与其他大学的联系，如美国的麦基梅隆大学和瑞典的斯德哥尔摩大学。

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.