Over the last century, logical and computational phenomena, in addition to more traditional physical ones, have provided mathematics with significant inspirations and been studied intensively. Today, as a consequence, mathematical logic and theoretical computer science have become mature as academic disciplines. From my (or a mathematician's) point of view, however, the very concepts of logic and computation have not been formulated in a completely satisfactory manner especially because they have been studied mostly by syntactic and/or synthetic methods; that is, something like topological spaces for topology (or the even more basic concept of sets for almost all traditional branches of mathematics) has been missing for logic and computation. My research is primarily concerned with this fundamental problem, and I aim to establish a mathematical, in particular semantic and analytic, foundation of logic and computation, whence of (constructive) mathematics as well.
I am also interested in category theory, more broadly algebra, and its interplay with logic and computation, known as categorical logic. My current focus on these fields is to generalize categorical algebra so that it corresponds to the generalization of propositional logic to predicate logic.
In addition, the recent advent of homotopy type theory has brought a novel, topological viewpoint into these fields. I am especially interested in such an interaction between logic, computation, category theory and topology.
Currently, I am about to complete my recent work on the unity of logic in terms of categorical algebra, proof theory and game semantics.
I have recently proved, by a novel game-semantic method, several open problems on the meta-theoretic study of Martin-Löf type theory in the context of constructive mathematics, e.g., consistency of Church's thesis.