Game-theoretic Interpretation of Intuitionistic Type Theory

TL;DR

This paper introduces a game semantics framework for intuitionistic type theory, providing an intuitive interpretation of dependent types and universes, advancing the understanding of computational and intensional aspects.

Contribution

It develops a novel category of games and strategies that generalize existing models, enabling an interpretation of complex type-theoretic constructs.

Findings

Provides a game semantics for dependent types and universes

Achieves an intuitive interpretation of type hierarchy

Advances the computational understanding of type theory

Abstract

We present a game semantics for intuitionistic type theory. Specifically, we propose categories with families of a new variant of games and strategies for both extensional and intensional variants of the type theory with dependent function, dependent pair, and identity types as well as universes. Our games and strategies generalize the existing notion of games and strategies and achieve an interpretation of dependent types and the hierarchy of universes in an intuitive manner. We believe that it is a significant step towards a computational and intensional interpretation of the type theory.