Game-theoretic Interpretation of Intuitionistic Type Theory
Logic in Computer Science
2016-10-05 v9 Discrete Mathematics
Combinatorics
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.
Keywords
Cite
@article{arxiv.1601.05336,
title = {Game-theoretic Interpretation of Intuitionistic Type Theory},
author = {Norihiro Yamada},
journal= {arXiv preprint arXiv:1601.05336},
year = {2016}
}
Comments
This paper has been withdrawn by the author because he has established a more reasonable game semantics for intuitionistic type theory