日本学術振興会賞

過去の受賞者について

第5回(平成20年度)日本学術振興会賞受賞者

photo_小林直樹
小林 直樹
(コバヤシ ナオキ)
KOBAYASHI Naoki



生年 1968年 出身地 愛知県
現職 東北大学大学院情報科学研究科 教授
(Professor, Graduate School of Information Sciences, Tohoku University)
専門分野 プログラム理論
略歴
1991年 東京大学理学部卒
1993年 東京大学大学院理学系研究科修士課程修了
1993年 日本学術振興会特別研究員-DC
1993年 東京大学大学院理学系研究科博士課程中退
1993年 東京大学大学院理学系研究科助手
1996年 博士(理学)の学位取得(東京大学)
1996年 東京大学大学院理学系研究科講師
2001年 東京工業大学大学院情報理工学研究科助教授
2004年 東北大学大学院情報科学研究科教授(現在に至る)

授賞理由
「ソフトウェア検証のための型理論」
(Type Theory for Software Verification)
 小林直樹氏は、コンピュータで扱うデータの「型」について独創的な理論的展開を行い、これをソフトウェアの検証に応用することで、情報処理の信頼性・安全性・効率を飛躍的に高めるための理論的基盤を構築した。
 同氏は、数理科学的な検証手法の中でも、特に型(タイプ)の理論に注目し、従来の「整数型」「実数型」「文字列型」などのデータの性質に基づく「型」の考え方を、「データがどのようにアクセスされるのか」にまで拡張することによって、並行して実行される多数のプログラムが本当に正しく動作しているかどうかを検証することを可能にした。また、同じく「型」の拡張によって、暗証番号などの機密情報の安全性に関する検証の理論を発展させ、さらに、プログラム実行の高速化のためのプログラム変換技術についても大きな質的向上をもたらした。
 同氏の業績は、理論的に奥深く独創的であるとともに、昨今大きな問題となっている情報インフラストラクチャの安全性・信頼性を飛躍的に高める技術としても高く評価できる。実社会に与える影響も極めて大きく、同研究の更なる発展が期待される。

第5回(平成20年度)日本学術振興会賞受賞者一覧へ戻る