Studies on logical structures of arithmetic and computation

田中沿着逆向数学的程序研究了证明一个普通数学定理需要多少集合论的知识。通过观察WKL_0的可数模型的性质，他（与T. Yamazaki和S. Simpson共同）证明了WKL_0对RCA_0的新守恒结果。Y. Akama介绍了一种组合逻辑的交集类型系统，并证明了它对于部分组合代数类是健全完备的。M. Horai已经证明，当引入高阶类型论的修正版本时，高阶直觉逻辑和构造演算之间的Curry-Howard同构可以更好地表述。她还研究了相对于简单类型系统的自由结构上的函数的lambda-可表示性，以及自由结构上的递归函数的概念。M. Tatsuta研究了单调共归纳定义的可实现性解释。他证明了，除其他外，全单调共归纳定义是不可靠的，而受限制的定义是可靠的。R. Hasegawa研究解析函数在理论计算机科学中的应用。鹿岛先生在相关逻辑上得到了几个重要的结果。

K. Tanaka studied along the program of reverse mathematics how much of set theory is needed to prove a theorem of ordinary mathematics. By observing properties of countable models of WKL_0, he proved (jointly with T. Yamazaki and S. Simpson) new conservation results of WKL_0 over RCA_0. Y. Akama introduced an intersection typing system for combinatory logic, and showed that it is sound and complete for the class of partial combinatory algebras. M. Horai has shown that the Curry-Howard isomorphism between higher-order intuitionistic logic and calculus of constructions can be better formulated when a modified version of higher-order type theory is introduced. She also studied the lambda-representability of functions over free structures with respect to the simple type system, as well as the notion of recursive functions over free-structures. M. Tatsuta investigated realizability interpretations of monotone coinductive definition. He proved, among others, that full monotone coinductive definitions are not sound while restricted ones are. R. Hasegawa studied applications of analytic functions to theoretical computer science. R. Kashima obtained several important results on relevant logic.