Dependent Type Theory and Game Semantics
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
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 study
A 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 on
Logic 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: Mathematical
Proceedings 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. on
p. 1).
2
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 study
A 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 on
Logic 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: Mathematical
Proceedings 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. on
p. 1).
2
Organisations
People |
ORCID iD |
| Samson Abramsky (Primary Supervisor) | |
| Samuel Speight (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509711/1 | 01/10/2016 | 30/09/2021 | |||
| 1893263 | Studentship | EP/N509711/1 | 01/10/2017 | 31/03/2021 | Samuel Speight |