Abstract: We present new game semantics of Martin-L"of type theory (MLTT) equipped with One-, Zero-, N-, Pi-, Sigma- and Id-types. Our game semantics interprets MLTT more accurately than existing ones. Another advantage of our game semantics over existing ones is its interpretation of Sigma-types that is direct and compatible with the game semantics of product types . Besides, its mathematical structure is novel and useful; e.g., the category of our games has all finite limits, which is a key step to an extension of the present work to homotopy type theory, and our games interpret subtyping on dependent types for the first time as game semantics. Finally, we provide a new, game-semantic proof of the independence of Markov's principle from MLTT, which demonstrates an advantage of our game semantics over extensional models of MLTT such as the effective topos.
Cites work
- A game semantics for generic polymorphism
- A game-semantic model of computation
- A semantics of evidence for classical arithmetic
- Abstract Böhm trees
- Constructivism in mathematics. An introduction. Volume II
- Domain interpretations of Martin-Löf's partial type theory
- Extensional and Intensional Semantic Universes
- Full abstraction for idealized Algol with passive expressions
- Full abstraction for PCF
- Game semantics for a polymorphic programming language
- Games and full completeness for multiplicative linear logic
- Games for dependent types
- Homotopy type theory. Univalent foundations of mathematics
- scientific article; zbMATH DE number 3825806 (Why is no real title available?)
- scientific article; zbMATH DE number 4012604 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 1229489 (Why is no real title available?)
- scientific article; zbMATH DE number 1241697 (Why is no real title available?)
- scientific article; zbMATH DE number 1259144 (Why is no real title available?)
- scientific article; zbMATH DE number 1302059 (Why is no real title available?)
- scientific article; zbMATH DE number 1302061 (Why is no real title available?)
- scientific article; zbMATH DE number 1342245 (Why is no real title available?)
- scientific article; zbMATH DE number 1497485 (Why is no real title available?)
- scientific article; zbMATH DE number 1499102 (Why is no real title available?)
- scientific article; zbMATH DE number 2110612 (Why is no real title available?)
- scientific article; zbMATH DE number 3248792 (Why is no real title available?)
- scientific article; zbMATH DE number 3291134 (Why is no real title available?)
- Internal type theory
- Lectures on the Curry-Howard isomorphism
- Linear logic
- Locally cartesian closed categories and type theory
- On full abstraction for PCF: I, II and III
- Sequential algorithms on concrete data structures
- The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
- The independence of Markov's principle in type theory
- Totality in arena games
This page was built for publication: Game semantics of Martin-Löf type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6190409)
