研究者紹介

Revision    1
2005. 3.31  現在      
 
【氏名】 たつた まこと
龍田   真
【生年月日】
1960年8月18日（満44才）
【博士号】
1993年、東京大学博士(理学)
【所属・役職】 教授
【電話番号】 03-4212-2552
【ファクシミリ】 03-3556-1916
【電子メールアドレス】 tatsuta AT nii.ac.jp
【個人ホームページ】 http://research.nii.ac.jp/~tatsuta
【専門分野】
理論計算機科学、数理論理学


◆ 研究概要
◆ 学歴
◆ 主要経歴
◆ 受賞等
◆ 教育活動歴
◆ 大学院担当講義
◆ 指導中の学生
◆ 学協会活動
◆ 社会貢献活動
◆ 重要論文・著書（上位10件）
◆ 重要活動の実績（上位10件）
◆ 査読付き論文／それらに相当する論文・著書 等
◆ 特許・公開ソフトウェア・作品等
◆ 上記に含まれない論文・記事・著作物等
◆ 講演・口頭発表等
◆ 教育指導等の実績
◆ 上記以外の業務活動実績
◆ 競争的研究資金獲得状況（公開）


【研究概要】

理論計算機科学と数理論理学を研究している。特に、プログラム理論と、 それに関連した数理論理学を研究している。プログラム理論では、特に、プロ グラム意味論、プログラム検証、プログラム合成、プログラム変換、計算モデ ル、型理論を研究している。また、数理論理学では、プログラム理論に関連し た論理、特に、証明論と構成的論理を研究し、また、その成果をプログラム理 論へ応用する研究を行っている。
【学歴】

1983年3月 東京大学法学部卒業

1985年3月 東京大学理学部情報科学科卒業

1987年3月 東京大学大学院理学系研究科情報科学専攻修士課程修了

1993年3月 東京大学博士(理学)
【主要経歴】

1989年4月 東北大学 電気通信研究所 助手

1994年10月 東北大学 電気通信研究所 助教授

1996年4月 京都大学 理学研究科 数学教室 助教授

2001年4月 国立情報学研究所 教授

2002年4月 総合研究大学院大学 教授(併任)
【受賞等】

1990年1月 日本ソフトウェア科学会 高橋奨励賞 受賞
【教育活動歴】

なし
【大学院担当講義】

情報論理学(総合研究大学院大学)

情報基盤科学概論(総合研究大学院大学)
【指導中の学生】

小合 敬之 (総合研究大学院大学 D3)

木村 大輔 (総合研究大学院大学 D2)
【学協会活動】

日本ソフトウェア科学会 会員 (1989--)

日本数学会 会員 (1995--)

Association for Symbolic Logic 会員 (1997--)

情報処理学会会員 (2002--)

情報処理学会の論文賞委員 (2004.11--2005.5)

情報処理学会の論文誌編集委員 (2002.5--)

日本数学会の数学基礎論サマースクールの講師(2001)

国際会議 Fourth International Symposium on Theoretical Aspects of Computer Software (2001) の program committee および session chairman

日本数学会2000年度秋季総合分科会 (2000) のプログラム委員

日本ソフトウェア科学会主催の国際会議 First JSSST Workshop on Programming and Programming Languages (1999) の program committeeおよび session chairman

日本ソフトウェア科学会主催の国際会議 Second JSSST Workshop on Programming and Programming Languages (2000) の program committeeおよび session chairman

日本ソフトウェア科学会第１３回大会 (1996) の座長

日本ソフトウェア科学会第１２回大会 (1995) の座長

電子情報通信学会のソフトウェアサイエンス研究専門委員会の委員 (1990.6--1995.5)

情報処理学会第４１回全国大会 (1990) の実行委員

日本ソフトウェア科学会チュートリアル「型理論」の講師 (1991)

日本ソフトウェア科学会チュートリアル「型理論と構成的プログラミング」の講師 (1997)

国際会議 Second International Symposium on Theoretical Aspects of Computer Software (1994) の session chair

国際会議 First International Symposium on Theoretical Aspects of Computer Software (1991) の local organizing committee

記号論理学と情報科学研究集会 (1991) の幹事(責任者)
【社会貢献活動】

情報処理振興事業協会のプログラムの演繹的導出法の調査研究に係るコンサルティング委員 (1990.6--1993.3)

新世代コンピュータ技術開発機構の記号計算ワーキンググループの委員 (1989.6--1990.3)

新世代コンピュータ技術開発機構の並列論証ワーキンググループの委員 (1990.4--1992.3)
【重要論文・著書（上位10件）】

  1. 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.

  2. M. Tatsuta, Program synthesis using realizability, Theoretical Computer Science 90 (1991) 309--353.

  3. M. Tatsuta, Realizability interpretation of coinductive definitions and program synthesis with streams, Theoretical Computer Science 122 (1994) 119--136.

  4. 龍田 真, 型理論, (近代科学社, 1992.11) 1--82.

  5. M. Tatsuta and G. Mints, A Simple Proof of Second Order Strong Normalization with Permutative Conversions, Annals of Pure and Applied Logic, to appear.

  6. 龍田 真, 構成的論理とプログラム理論, 1998年度日本数学会秋季総合分科会総合講演企画特別講演アブストラクト (1998) 13--24.

  7. 小林 聡, 龍田 真, 直観主義的帰納的定義に対する実現可能性解釈, ソフトウェア科学会第６回全国大会論文集 (1989) 113--116.

  8. Makoto Tatsuta, Realizability of Inductive Definitions for Constructive Programming, Doctoral Dissertation, University of Tokyo, 1993.

  9. 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.

  10. M. Tatsuta, Uniqueness of Normal Proofs of Minimal Formulas, Journal of Symbolic Logic 58 (3) (1993) 789--799.

【重要活動の実績（上位10件）】

  1. M. Tatsuta, Proof Figure Macros proof.sty, http://research.nii.ac.jp/~tatsuta/proof-sty.html (1990).

  2. M. Tatsuta and G. Mints, A simple proof of strong normalization with permutative conversions, Stanford Logic Seminar (2004).

  3. M. Tatsuta, Martin-Lof's type theory with permutative reductions, Stanford Logic Seminar (2004).

  4. 龍田 真, 中澤 巧, CPS変換による強正規化性の証明, Second JSSST workshop on Programming and Programming Languages (2000).

【査読付き論文／それらに相当する論文・著書 等】

  1. 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.

  2. M. Tatsuta, Program synthesis using realizability, Theoretical Computer Science 90 (1991) 309--353.

  3. M. Tatsuta, Realizability Interpretation of Coinductive Definitions and Program Synthesis with Streams, Proceedings of International Conference on Fifth Generation Computer Systems} (1992) 666--673.

  4. M. Tatsuta, Uniqueness of Normal Proofs of Minimal Formulas, Journal of Symbolic Logic 58 (3) (1993) 789--799.

  5. Makoto Tatsuta, Realizability of Inductive Definitions for Constructive Programming, Doctoral Dissertation, University of Tokyo, 1993.

  6. M. Tatsuta, Realizability interpretation of coinductive definitions and program synthesis with streams, Theoretical Computer Science 122 (1994) 119--136.

  7. M. Tatsuta, Two realizability interpretations of monotone inductive definitions, International Journal of Foundations of Computer Science 5 (1) (1994) 1--21.

  8. S. Kobayashi and M. Tatsuta, Realizability interpretation of generalized inductive definitions, Theoretical Computer Science 131 (1) (1994) 121--138.

  9. M. Tada and M. Tatsuta, The Function [a/m] in Sharply Bounded Arithmetic, Archive for Mathematical Logic 37 (1997) 51--57.

  10. 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.

  11. 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.

  12. 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.

  13. M. Tatsuta, Uniqueness of D-normal Proofs, Proceedings of 7th Asian Logic Conference (1999) 41--42.

  14. S. Hirokawa and M. Tatsuta, Long D-normal form yields uniqueness of proofs, Proceedings of 2000 European Congress of Association for Symbolic Logic (2000)

  15. 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.

  16. M. Tatsuta and G. Mints, A Simple Proof of Second Order Strong Normalization with Permutative Conversions, Annals of Pure and Applied Logic, to appear.
【特許・公開ソフトウェア・作品等】

  1. M. Tatsuta, Proof Figure Macros proof.sty, http://research.nii.ac.jp/~tatsuta/proof-sty.html (1990).

【上記に含まれない論文・記事・著作物等】

  1. 小林 聡, 龍田 真, 直観主義的帰納的定義に対する実現可能性解釈, ソフトウェア科学会第６回全国大会論文集 (1989) 113--116.

  2. 龍田 真, 書評: J.Y. Girard et al 著 Proofs and Types ( Cambridge Univ Press, 1989), 情報処理学会誌, 1990年8月号.

  3. 龍田 真, 型理論 I, コンピュータソフトェア 8 (1) (1991) 25--33.

  4. 龍田 真, 型理論 II, コンピュータソフトェア 8 (2) (1991) 40--46.

  5. 龍田 真, 型理論 III, コンピュータソフトェア 8 (3) (1991) 2--8.

  6. 龍田 真, 型理論 IV, コンピュータソフトェア 8 (4) (1991) 56--68.

  7. 龍田 真, 型理論, (近代科学社, 1992.11) 1--82.

  8. 龍田 真 (分担執筆)、情報処理学会編, 新版情報処理ハンドブック, 第1編第3章第2節,オーム社 (1995).

  9. 龍田 真, 構成的集合の実現可能性解釈, 日本ソフトウェア科学会第15回大会論文集 (1998) 189--192.

  10. 龍田 真, 構成的論理とプログラム理論, 1998年度日本数学会秋季総合分科会総合講演企画特別講演アブストラクト (1998) 13--24.

  11. 龍田 真, 構成的集合論の実現可能性とそのプログラム合成への応用, Proceedings of First JSSST workshop on Programming and Programming Languages (1999) 139--143.

  12. 龍田 真 (分担執筆)、日本数学会編、岩波数学辞典第４版, 型理論とλ計算, 岩波書店, 出版予定.

  13. 龍田 真, G. Mints, 置換簡約をもつ二階自然演繹の強正規化可能性, 2005年度日本数学会年会アブストラクト (2005).
【講演・口頭発表等】

  1. 龍田 真, 中澤 巧, CPS変換による強正規化性の証明, Second JSSST workshop on Programming and Programming Languages (2000).

  2. M. Tatsuta and G. Mints, A simple proof of strong normalization with permutative conversions, Stanford Logic Seminar (2004).

  3. M. Tatsuta, Martin-Lof's type theory with permutative reductions, Stanford Logic Seminar (2004).

【教育指導等の実績】

  1. 大学院修士4名(1994--)

  2. 大学院博士1名(1994--)

  3. 東京工業大学の非常勤講師 (1997)

  4. 筑波大学の非常勤講師 (1999)

  5. 東京大学の非常勤講師 (2000--2002)
【上記以外の業務活動実績】

  1. なし
【競争的研究資金獲得状況（公開）】

  (1) 科研費

  • 平成４年度科学研究費補助金奨励研究(A) (平成４年度:９０万円) 　　「帰納的定義を用いたプログラム合成」
  • 平成５年度科学研究費補助金奨励研究(A) (平成５年度:９０万円) 　　「帰納的定義を用いたプログラム合成」
  • 平成６年度科学研究費補助金奨励研究(A) (平成６年度:９０万円) 　　「帰納的定義を用いたプログラム合成」
  • 平成７年度科学研究費補助金奨励研究(A) (平成７年度:１１０万円) 　　「帰納的定義を用いたプログラム合成」
  • 平成８年度科学研究費補助金奨励研究(A) (平成８年度:１１０万円) 　　「帰納的定義を用いたプログラム合成」
  • 平成９年度科学研究費補助金奨励研究(A) (平成９－１０年度:２４０万円) 　　「帰納的定義を用いたプログラム合成」
  • 平成１２年度科学研究費補助金基盤研究(C) (平成１２－１５年度) 　　「構成的集合と余帰納的定義を用いたプログラム合成 」
  (2) 科研費以外の政府関係の研究費

  なし
  (3) その他の研究費

  • 平成６年(１９９４年)度　研究助成(カシオ科学振興財団):１００万円
  • 平成７年(１９９５年)度　研究助成（電気通信普及財団）：１００万円
  • 平成８年(１９９６年)度　研究助成（大川情報通信基金）：１００万円
  • 平成１１年（１９９９年）度　研究助成（栢森情報科学振興財団）：５０万円