Homotopy Type Theory in Game Semantics

游戏语义中的同伦类型论

• 批准号: 2218874
• 金额: --
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2019
• 资助国家: 英国
• 起止时间: 2019 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2218874
• 关键词: Homotopy; Type; Theory; 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.

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