ISHIHARA, Hajime Professor
School of Information Science,Intelligent Robotics Area
B.S., M.S. and Ph.D.from Tokyo Institute of Technology (1980,1987,1990)
◆Professional Experience
: Researcher at Mitsubishi Research Institute, Inc. (1980), Associate at Hiroshima University (1988), Associate Professor at Japan Advanced Institute of Science and Technology (1992)
Constructive Mathematics, Mathematical Logic, and Foundations of Mathematics
◆Research Keywords
intuitionistic logic, reverse mathematics, constructive set theory
◆Research Interests
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-Loef 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.


◆Published Papers
Consistency of the intensional level of the Minimalist Foundation with Church's thesis and axiom of choice.
Hajime Ishihara,Maria Emilia Maietti,Samuele Maschio,Thomas Streicher
Arch. Math. Log., 57, 7-8, 873-888, 2018
Preface to the special issue: Continuity, computability, constructivity: from logic to algorithms 2013.
Hajime Ishihara,Margarita V. Korovina,Arno Pauly,Monika Seisenberger,Dieter Spreen
Mathematical Structures in Computer Science, 27, 8, 1285-1286, 2017
Embedding classical in minimal implicational logic.
Hajime Ishihara,Helmut Schwichtenberg
Math. Log. Q., 62, 1-2, 94-101, 2016
A note on the independence of premiss rule.
Hajime Ishihara,Takako Nemoto
Math. Log. Q., 62, 1-2, 72-76, 2016
Completeness and cocompleteness of the categories of basic pairs and concrete spaces.
Hajime Ishihara,Tatsuji Kawai
Mathematical Structures in Computer Science, 25, 8, 1626-1648, 2015
◆Conference Activities & Talks
A monad on the combinatory algebras
Hajime Ishihara
Operations, Sets, and Types, Muenchenwiler, Switzerland, 2016/04/18
Constructive reverse mathematics: an introduction and recent results
Hajime Ishihara
Frontiers of Non-Classicality: Logic, Mathematics, Philosophy, Auckland, New Zealand, 2016/01/26
Constructive reverse mathematics and omniscience pringiples
Hajime Ishihara
14th Asian Logic Conference, Munbai, India, 2015/01/05
Intuitionistic logic and reverse mathematics
Hajime Ishihara
Proof, Truth, Computation: Summer School on the Interactions between Modern Foundations of Mathematics and Contemporary Philosophy, Chiemsee, Germany, 2014/07/21
A monad in the combinatory algebras
Hajime Ishihara
Correctness by Construction CORCON 2014 Workshop, Genoa, Italy, 2014/03/24

■Teaching Experience

Fundamentals of Logic and Mathematics, Mathematical Logic(E), Theoretical Computer Science, Computation Theory(E)

■Contributions to  Society

◆Academic Society Affiliations
Mathematical Society of Japan, American Mathematical Society, Association for Symbolic Logic
◆Academic Contribution
Workshop on Constructive Aspects of Logic and Mathematics , Japan Advanced Institute of Science and Technology, School of Information Science, Associate Professor Hajime Ishihara , 2010/03/08 - 2010/03/12 , Kanazawa
Workshop on Constructivism: Logic and Mathematics , Japan Advanced Institute of Science and Technology, School of Information Science, Associate Professor, Hajime Ishihara , 2008/05/26 - 2008/05/30 , Kanazawa