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 yet been captured in a completely satisfactory manner especially because they have been studied mostly by syntactic and/or synthetic methods. 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.
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 formulating the very concepts of the unity, the duality, the linearity and the intuitionisity of logic and computation in terms of categorical algebra, proof theory and theory of computation.