Dependent Type Theory and Game Semantics

这个项目属于EPSRC‘信息和通信技术’主题，特别是‘理论计算机科学’研究领域。依赖类型理论(DTT)(简单类型lambda演算的扩展)引起计算机科学家和数学家的兴趣有几个原因：与lambda演算相比，它可以被视为一种更具表现力的编程语言，并形成了许多证明辅助工具的基础，如Coq和Lean。此外，它越来越多地被认为是数学的基础语言，也是一种更忠实于数学实践的语言。尤其是随着同伦类型理论(Hott)[Uni13]的出现，DTT之所以被称为DTT，是因为它承认[AW09]的同伦解释。在这个项目中，我们将研究DTT的语义。这已经是一个久负盛名的领域，尽管有许多有趣的开放方向。在Abramsky，Jagadeesan和Vákár最近的工作中，给出了DTT的第一个游戏语义[AJV15]。游戏语义学的想法是将计算建模为游戏中的交替玩法。因此，这些直觉与前面提到的DTT同伦解释背后的那些不同(以及其他更空间上，而不是时间上的灵感解释)。然而，这突显了研究形式系统的语义的强烈动机：在这样做的过程中，人们可能会发现所谓的互不相连的结构和框架之间的富有成效的联系。此外，对语义学的研究可以在逻辑方面带来创新。事实上，正是对DTT的同伦解释启发了沃沃茨基的单价公理。希望通过对游戏语义学的继续研究，实现这样的联系和创新。与以上相关的一个具体目标是找到一个满足单价公理的DTT的博弈模型。[AJV15]中给出的模型满足身份证明的唯一性原则，如果要满足单价证明，则需要打破这一原则。此外，博弈语义学一直被认为是“一种具有稳健数学结构的内涵结构的积极理论”[ABR14]，因此有理由认为它可能能够提供对单价性的计算解释。内涵性、可定义性和计算性。摘自：约翰·范·本瑟姆的《逻辑与信息动力学》。Springer，2014，第121-142页(同上)第1页)。[AJV15]Samson Abramsky，Radha Jagadeesan和Matthijs Vákár。“依赖类型的游戏”。收录：自动机、语言和编程国际学术讨论会。斯普林格。2015年，第31-43页(同上)第1页)[AW09]史蒂夫·阿沃迪和迈克尔·A·沃伦。身份类型的同伦理论模型。见：《数学剑桥哲学学会论文集》146(2009)，第45-55页(同上)。见第1页)。[Uni13]单价基金会计划。同伦类型理论：数学的单价基础。高级研究院：https://homotopytypetheory.org/book，2013年(同上。国家石油公司。1).2

This project falls within the EPSRC 'information and communication technologies' theme and specifically the 'theoretical computer science' research area.Dependent type theory (DTT) (an extension of the simply typed lambda-calculus) is of interest to computer scientists and mathematicians for a number of reasons: It can be seen as a more expressive-compared to the lambda-calculus-programming language and forms the basis for a number of proofs assistants, such as Coq and Lean. Furthermore, it is increasingly being considered as a foundational language for mathematics-and one that is more faithful to mathematical practice. This is especially so with the emergence of homotopy type theory (HoTT) [Uni13], a DTT so called due to the homotopical interpretation it admits [AW09].In this project we will study the semantics of DTT. This is already a well-established field, though one with many interesting open directions. In recent work of Abramsky, Jagadeesan and Vákár, the first game semantics of DTT is given [AJV15]. The idea of game semantics is to model computation as alternating plays in a game. The intuitions are thus different to those behind the aforementioned homotopical interpretation of DTT (and other more spatially, rather than temporally, inspired interpretations). However, this highlights a strong motivation for studying the semantics of formal systems: in doing so, one may discover fruitful connections between supposed disconnected structures and frameworks. Moreover, the study of semantics can lead to innovations back on logic side. Indeed, it was the homotopical interpretation of DTT that inspired Voevodsky's univalence axiom. It is the hope that by continuing the study of game semantics, such connections and innovations will be made. In particular, we wish to emphasise categorical aspects of the studyA concrete aim in relation to the above is to find a game model of DTT satisfying the univalence axiom.The model given in [AJV15] satisfies the principle of uniqueness of identity proofs, which would need to be broken if univalence is to be satisfied. Moreover, game semantics has been regarded as "a positive theory of intensional structures with a robust mathematical structure" [Abr14], and so it is reasonable to think thatit may be able to provide a computational interpretation of univalence.References[Abr14] Samson Abramsky. "Intensionality, definability and computation". In: Johan van Benthem onLogic and Information Dynamics. Springer, 2014, pp. 121-142 (cit. on p. 1).[AJV15] Samson Abramsky, Radha Jagadeesan, and Matthijs Vákár. "Games for dependent types". In:International Colloquium on Automata, Languages, and Programming. Springer. 2015, pp. 31-43(cit. on p. 1).[AW09] Steve Awodey and Michael A. Warren. "Homotopy theoretic models of identity types". In: MathematicalProceedings of the Cambridge Philosophical Society 146 (2009), pp. 45-55 (cit. on p. 1).[Uni13] Ther Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics.Institute for Advanced Study: https://homotopytypetheory.org/book, 2013 (cit. onp. 1).2