Norihiro Yamada: Game Semantics of Martin-Löf Type Theory

Abstract: In this talk, I present my work on game semantics of Martin-Löf Type Theory (MLTT).

Game semantics has been a highly successful approach to semantics of logic (and computation), which interprets proofs as “dialogical arguments” of a prover mathematician against a refuter mathematician in a mathematically precise, conceptually natural and syntax-independent manner. Surprisingly, however, game semantics of MLTT has been missing for two decades due to the difficulty in modeling type dependency in terms of games. In fact, there has been only one game semantics of dependent types by Abramsky et al. established in 2015, but it is not a complete solution either: Its interpretation of sigma-types is not by games but by a general list-construction, and it does not interpret universes at all.

In this context, I have developed a game semantics of MLTT equipped with 1-, 0-, N-, pi-, sigma- and Id-types as well as a cumulative hierarchy of universes. Notably, it models every type construction (including sigma-types and universes) solely in terms of games. I have extended it further to capture proof-normalization and (higher-order) computability of MLTT. I have also equipped it with the groupoid structure so that it refutes uniqueness of identity proofs (UIP) for the first time as game semantics, which foresees its connection with Homotopy Type Theory (HoTT).

I assume that audiences are familiar with MLTT but not game semantics. I shall rather focus on main ideas and points, leaving the details to references.