Our research area is an interdisciplinary area between mathematics and computer science. It is classified into mathematical logic or foundations of mathematics, as mathematics, and into theoretical computer science, as computer science. We have been especially focusing on constructive mathematics, mathematical logic, and theory of computation.

Constructive Mathematics

We have been exploring constructive mathematics as mathematics with intuitionistic logic which originated in Brouwer’s intuitionistic mathematics and formalized by Heyting and Kolmogorov. We have been dealing with constructive functional analysis such as theory of Hilbert and Banach spaces and theory of distributions, and with constructive topological spaces such as neighbourhood spaces, formal topology, and basic pair. As a foundation of constructive mathematics, we have also been studying constructive set theory (CZF) which is a predicative system and has a quite natural interpretation in Martin-Löf type theory. Furthermore, we have been advocating, and leading a research on, constructive reverse mathematics which aims at classifying, arranging and systematizing mathematical theorems, in classical mathematics, Brouwer’s intuitionistic mathematics and constructive recursive mathematics developed under different philosophies of mathematics, by logical principles and/or function existence axioms from a uniform point of view.

Mathematical Logic

We have been studying proof theory and semantics of intuitionisitc logic. Since there is a natural correspondence, called the Curry-Howard correspondence, between proofs in intuitionistic logic and programs (terms of lambda-calculus), we are able to extract programs from proofs in intuitionistic logic, and program extraction systems, based on this fact, such as the Minlog system at University of Munich, has been developed. We have been dealing with relationship between classical logic and intuitionistic logic, and doing a research on extracting programs from constructive contents of classical proofs. Also we have been studying proof theory and semantics of substructural logics such as linear logic.

Theory of Computation

We have been studying computability theory and computational complexity theory, and relationship between them and constructive mathematics. We have been characterizing classes of computable functions, such as the class of polynomial time computable functions, as function algebras, and trying to explore relationship between computational complexity and degrees of unsolvability, and logical principles and function existence axioms in constructive reverse mathematics. Furthermore, we have been dealing with lambda-calculus and type theory such as simple types, intersection types and union types.

Theoretical study is done independently and voluntary based on being conscious of points and problems in the study. We have been respecting and encouraging independent and voluntary study of each student. Please look into here, if you are interested in study in our laboratory.

Research topics for the Master Program include constructive mathematics, mathematical logic, category theory, lambda-calculus, computational complexity, algorithmic information theory, quantum computation, automata theory, and formal languages. The following people finished the Doctor Program under supervisions of Professor Ishihara.

• Professor Takahito Aoto (Professor, Niigata University), On some characterizations of implicational formulas in intuitionistic logic, 1997.
• Dr. Norihiro Kamide (Associate Professor, Teikyo University), Substructural logics with restricted versions of structural rules, 2000.
• Dr. Katsumasa Ishii, Proof theoretical investigations for Visser’s logic, classical logic and the first-order arithmetic, 2002.
• Dr. Kentaro Kikuchi (Assistant Professor, Tohoku University), Gentzen style sequent calculi for some subsystems of intuitionistic logic, 2002.
• Dr. Satoru Yoshida (Associate Professor, Tottori University of Environmental Studies), A constructive study of the fundamental theory of distributions, 2003.
• Dr. Tatsuji Kawai (Assistant Professor, JAIST), Bishop compactness in formal topologies, 2015.
• Dr. Satoru Niki (Postdoctoral Researcher, Ruhr-Universität Bochum）, Investigations into intuitionistic and other negations, 2021.