1 citations · 2 across the 14 of their papers we have counts for
14 papers
Logic and computation as combinatorics
Norihiro Yamada
The syntactic nature of logic and computation separates them from other fields of mathematics. Nevertheless, syntax has been the only way to adequately capture the dynamics of proo…
Game semantics of universes
Norihiro Yamada
This work extends the present author's computational game semantics of Martin-Löf type theory to the cumulative hierarchy of universes. This extension completes game semantics of a…
Game semantics of Martin-Löf type theory, part III: its consistency with Church's thesis
Norihiro Yamada
We prove consistency of intensional Martin-Löf type theory (MLTT) with formal Church's thesis (CT), which was open for at least fifteen years. The difficulty in proving the consist…
Sequent calculi for a unity of logic
Norihiro Yamada
We present a novel unity of logic, viz., a single sequent calculus that embodies classical, intuitionistic and linear logics. Concretely, we define classical linear logic negative…
On the Unity of Logic: a Sequential, Unpolarized Approach
Norihiro Yamada
The present work aims to give a unity of logic via standard sequential, unpolarized games. Specifically, our vision is that there must be mathematically precise concepts of linear…
Game Semantics of Martin-Löf Type Theory
Norihiro Yamada
We present new game semantics of Martin-Löf type theory (MLTT) equipped with One-, Zero-, N-, Pi-, Sigma- and Id-types. Our game semantics interprets MLTT more accurately than exis…
A Game-Semantic Model of Computation, Revisited: an Automata-Theoretic Perspective
Norihiro Yamada
In the previous work, we have given a novel, game-semantic model of computation in an intrinsic, non-inductive and non-axiomatic manner, which is similar to Turing machines but bey…
Game-theoretic Investigation of Intensional Equalities
Norihiro Yamada
This article presents a new game semantics for Martin-Löf type theory (MLTT), in which each game is equipped with selected isomorphism strategies that represent (computational) pro…
Categories with Dependence and Semantics of Dependent Types
Norihiro Yamada
The present paper gives a generalization of cartesian closed categories, called cartesian closed categories with dependence, whose strict version induces categories with families t…
A Game-Semantic Model of Computation
Norihiro Yamada
The present paper introduces a novel notion of `(effective) computability', called viability, of strategies in game semantics in an intrinsic (i.e., without recourse to the standar…
Game Semantics for Martin-Löf Type Theory
Norihiro Yamada
We present a new game semantics for Martin-Löf type theory (MLTT), our aim is to give a mathematical and intensional explanation of MLTT. Specifically, we propose a category with f…
Game-theoretic Interpretation of Type Theory Part II: Uniqueness of Identity Proofs and Univalence
Norihiro Yamada
In the present paper, based on the previous work (Part I), we present a game semantics for the intensional variant of intuitionistic type theory that refutes the principle of uniqu…
Game-theoretic Interpretation of Intuitionistic Type Theory
Norihiro Yamada
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 inte…
Dynamic Game Semantics
Norihiro Yamada, Samson Abramsky
The present paper gives a mathematical, in particular, syntax-independent, formulation of intensionality and dynamics of computation in terms of games and strategies. Specifically,…