Homotopy Type Theory in Game Semantics

该项目属于EPSRC研究领域“编程语言和编译器”和“理论计算机科学”。近年来出现了一种新的形式语言，同伦类型理论（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.