Introduction of researcher

Revision 1

As of 2005. 3.31

[Name]	TATSUTA Makoto
[Date of birth]	1960/8/18 (44 years old)
[Doctoral degrees]	1993, PhD., University of Tokyo
[Affiliation / Position]	Professor
[Telephone]	+81-3-4212-2552
[Facsimile]	+81-3-3556-1916
[E-mail]	tatsuta AT nii.ac.jp
[Personal home page]	http://research.nii.ac.jp/~tatsuta/index-e.html
[Research fields]	Theoretical Computer Science, Mathematical Logic


<>	Outline of current research
<>	Education
<>	Career
<>	Awards
<>	Teaching positions
<>	Courses
<>	Students
<>	Academic societies
<>	Public activities
<>	Most important publications (Top 10)
<>	Most important activities (Top 10)
<>	Refereed publications, published books
<>	Patents / softwares / other works
<>	Other publications
<>	Speeches and oral presentations
<>	Teaching experience
<>	Other activities in the past
<>	Competitive research funds

[Outline of current research]
	I'm interested in theoretical computer science and mathematical logic. Specifically I'm studing theory of programs and mathematical logic related to it. My work on theory of programs includes program semantics, program verification, program synthesis, program transformation, computational models, and type theory. My work on mathematical logic includes proof theory, constructive logic, and their application to theory of programs.
[Education]
	BS in Law from the Univ of Tokyo in 1983 BS in Information Science from the Univ of Tokyo in 1985 MS in Information Science from the Univ of Tokyo in 1987 PhD from the Univ of Tokyo in 1993
[Career]
	Research Associate, RIEC, Tohoku Univ in 1989 Associate Professor, RIEC, Tohoku Univ in 1994 Associate Professor, Dept of Mathematics, Kyoto Univ in 1996 Professor, National Institute of Informatics in 2001 (Concurrent position) Professor, The Graduate University for Advanced Studies
[Awards]
	none
[Teaching positions]
	none
[Courses]
	Logic in Computer Science (The Graduate University for Advanced Studies) Foundations of Informatics (The Graduate University for Advanced Studies)
[Students]
	KOAI, Takayuki (The Graduate University for Advanced Studies, D3) KIMURA, Daisuke (The Graduate University for Advanced Studies, D2)
[Academic societies]
	a member of Japan Society for Software Science and Technology (1989--) a member of the Mathematical Society of Japan (1995--) a member of Association for Symbolic Logic (1997--) a member of Information Processing Society of Japan (2002--) a Journal Editorial Board member of Information Processing Society of Japan (2002.5--) a lecturer of Foundations of Mathematics Summer School by the Mathematical Society of Japan (2001) a program committee member and a session chairman of Fourth International Symposium on Theoretical Aspects of Computer Software (2001) a program committee member of 2000 Annual Fall Conference of the Mathematical Society of Japan (2000) a program committee member and a session chairman of First JSSST Workshop on Programming and Programming Languages by Japan Society for Software Science and Technology (1999) a program committee member and a session chairman of Second JSSST Workshop on Programming and Programming Languages by Japan Society for Software Science and Technology (2000) a session chairman of Thirteenth Annual Conference of Japan Society for Software Science and Technology (1996) a session chairman of Twelfth Annual Conference of Japan Society for Software Science and Technology (1995) a software science research committee member of the Institute of Electronics, Information and Communication Engineers (1990.6--1995.5) an organizing committee member of 41th Annual Conference of Information Processing Society of Japan (1990) a lecturer of tutorial "type theory" by Japan Society for Software Science and Technology (1991) a lecturer of tutorial "type theory and constructive programming" by Japan Society for Software Science and Technology (1997) a session chairman of Second International Symposium on Theoretical Aspects of Computer Software (1994) a local organizing committee member of First International Symposium on Theoretical Aspects of Computer Software (1991) a chairman of Symbolic Logic and Information Science Workshop (1991)
[Public activities]
	a consulting committee member of research on deductive method of programming by Information-technology Promotion Agency (1990.6--1993.3) a symbolic computation working group member of Institute for New Generation Computer Technology (1989.6--1990.3) a concurrent proving working group member of Institute for New Generation Computer Technology (1990.4--1992.3)
[Most important publications (Top 10)]
	M. Tatsuta, Realizability for Constructive Theory of Functions and Classes and Its Application to Program Synthesis, Proceedings of Thirteenth Annual IEEE Symposium on Logic in Computer Science (1998) 358--367. M. Tatsuta, Program synthesis using realizability, Theoretical Computer Science 90 (1991) 309--353. M. Tatsuta, Realizability interpretation of coinductive definitions and program synthesis with streams, Theoretical Computer Science 122 (1994) 119--136. M. Tatsuta and G. Mints, A Simple Proof of Second Order Strong Normalization with Permutative Conversions, Annals of Pure and Applied Logic, to appear. Makoto Tatsuta, Realizability of Inductive Definitions for Constructive Programming, Doctoral Dissertation, University of Tokyo, 1993. K. Nakazawa and M. Tatsuta, Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction, Journal Symbolic of Logic 68 (3) (2003) 851--859. M. Tatsuta, Uniqueness of Normal Proofs of Minimal Formulas, Journal of Symbolic Logic 58 (3) (1993) 789--799. M. Tada and M. Tatsuta, The Function [a/m] in Sharply Bounded Arithmetic, Archive for Mathematical Logic 37 (1997) 51--57. S. Kobayashi and M. Tatsuta, Realizability interpretation of generalized inductive definitions, Theoretical Computer Science 131 (1) (1994) 121--138. M. Tatsuta, Two realizability interpretations of monotone inductive definitions, International Journal of Foundations of Computer Science 5 (1) (1994) 1--21.
[Most important activities (Top 10)]
	M. Tatsuta, Proof Figure Macros proof.sty, http://research.nii.ac.jp/~tatsuta/proof-sty.html (1990). M. Tatsuta and G. Mints, A simple proof of strong normalization with permutative conversions, Stanford Logic Seminar (2004). M. Tatsuta, Martin-Lof's type theory with permutative reductions, Stanford Logic Seminar (2004).
[Refereed publications, published books]
	M. Tatsuta,Monotone Recursive Definition of Predicates and Its Realizability Interpretation, Proceedings of International Conference on Theoretical Aspects of Computer Software, LNCS 526 (1991) 38--52. M. Tatsuta, Program synthesis using realizability, Theoretical Computer Science 90 (1991) 309--353. M. Tatsuta, Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams, Proceedings of International Conference on Fifth Generation Computer Systems} (1992) 666--673. M. Tatsuta, Uniqueness of Normal Proofs of Minimal Formulas, Journal of Symbolic Logic 58 (3) (1993) 789--799. Makoto Tatsuta, Realizability of Inductive Definitions for Constructive Programming, Doctoral Dissertation, University of Tokyo, 1993. M. Tatsuta, Realizability interpretation of coinductive definitions and program synthesis with streams, Theoretical Computer Science 122 (1994) 119--136. M. Tatsuta, Two realizability interpretations of monotone inductive definitions, International Journal of Foundations of Computer Science 5 (1) (1994) 1--21. S. Kobayashi and M. Tatsuta, Realizability interpretation of generalized inductive definitions, Theoretical Computer Science 131 (1) (1994) 121--138. M. Tada and M. Tatsuta, The Function [a/m] in Sharply Bounded Arithmetic, Archive for Mathematical Logic 37 (1997) 51--57. M. Tatsuta, Uniform Continuity of Graph Model and Partial Function Model, Proceedings of 1997-98 Annual Meeting of Association for Symbolic Logic (1998) 20--21. M. Tatsuta, Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis, Proceedings of Fourth International Conference on Mathematics of Program Construction, LNCS 1422 (1998) 338--364. M. Tatsuta, Realizability for Constructive Theory of Functions and Classes and Its Application to Program Synthesis, Proceedings of Thirteenth Annual IEEE Symposium on Logic in Computer Science (1998) 358--367. M. Tatsuta, Uniqueness of D-normal Proofs, Proceedings of 7th Asian Logic Conference (1999) 41--42. S. Hirokawa and M. Tatsuta, Long D-normal form yields uniqueness of proofs, Proceedings of 2000 European Congress of Association for Symbolic Logic (2000) K. Nakazawa and M. Tatsuta, Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction, Journal Symbolic of Logic 68 (3) (2003) 851--859. M. Tatsuta and G. Mints, A Simple Proof of Second Order Strong Normalization with Permutative Conversions, Annals of Pure and Applied Logic, to appear.
[Patents / softwares / other works]
	M. Tatsuta, Proof Figure Macros proof.sty, http://research.nii.ac.jp/~tatsuta/proof-sty.html (1990).
[Other publications]
	none
[Speeches and oral presentations]
	M. Tatsuta and G. Mints, A simple proof of strong normalization with permutative conversions, Stanford Logic Seminar (2004). M. Tatsuta, Martin-Lof's type theory with permutative reductions, Stanford Logic Seminar (2004).
[Teaching experience]
	Supervisor of four graduate students in master course(1994--) Supervisor of one graduate student in PhD course(1994--) Part-time lecturer of Tokyo Institute of Technology (1997) Part-time lecturer of Tsukuba University (1999) Part-time lecturer of University of Tokyo (2000--2002)
[Other activities in the past]
	None
[Competitive research funds]
(1) Grant in aid for scientific research
	Grant-in-Aid for Encouragement of Young Scientists (A) 1992 “Program synthesis using inductive definitions” Grant-in-Aid for Encouragement of Young Scientists (A) 1993 “Program synthesis using inductive definitions” Grant-in-Aid for Encouragement of Young Scientists (A) 1994 “Program synthesis using inductive definitions” Grant-in-Aid for Encouragement of Young Scientists (A) 1995 “Program synthesis using inductive definitions” Grant-in-Aid for Encouragement of Young Scientists (A) 1996 “Program synthesis using inductive definitions” Grant-in-Aid for Encouragement of Young Scientists (A) 1997 (to 1998) “Program synthesis using inductive definitions” Grant-in-Aid for Scientific Research (C) 2000 (to 2003) “Program synthesis using constructive sets and coinductive definitions”
(2) Public funding
	none
(3) Others
	Scientific Research Aid 1999