表彰等

2010年度基礎研究賞

2010年度基礎研究賞の授与について

理事長 柴山 悦哉

日本ソフトウェア科学会は,ソフトウェア科学分野の基礎研究において顕著な業績を挙げられた研究者に対して,基礎研究賞を授与し,その功績を称える制度を2008年度に設けました.基礎研究賞は毎年2件程度の業績に対して,主要な貢献のあった研究者に対し
て賞状および副賞を授与するものです.第3回にあたる2010年度は,2011年2月18日に開催された基礎研究賞選定委員会の審議結果を受け,同年3月のメイル理事会において2件の研究に対して基礎研究賞を授与することとしました.

選定委員会の構成は以下の通りです.

柴山 悦哉(理事長),本位田 真一(編集委員長)
大沢 英一,加藤 和彦,砂原 秀樹,萩谷 昌己,安村 通晃.

 

大堀 淳 氏 (東北大学電気通信研究所)


授賞業績: 型システムを用いたプログラミング言語実現に関する研究
授賞理由:

大堀氏は,1980年代後半から90年代の始めにプログラミング言語研究の主要なテーマの一つであった多相レコードについて,その実用的コンパイル手法をはじめて考案した.この研究によって導入されたカインドを用いた多相性とそのコンパイル手法は拡張性・応用性が非常に高く,型主導コンパイルと呼ばれる研究分野を開拓する先駆的な研究であった.
この研究は,1992年にプログラミング言語に関する最高峰の国際会議POPLで,さらにその雑誌版が権威ある論文誌TOPLASで発表され,現在までに100編以上の論文に引用され(citeseerx.ist.psu.eduによる),国際的に非常に高い評価を得えている.その後も同氏は,この分野の研究を精力的に続け,コンパイラのバックエンドまで対象を広げた基礎的かつ独創的成果,SML#コンパイラの実装のような実用的な成果などを得ている.よって,日本ソフトウェア科学会は大堀淳氏に基礎研究賞を授与することとした.

出典:

Atsushi Ohori: A Compilation Method for ML-Style Polymorphic Record Calculi, Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 154--165, 1992. (Journal Version: Atsushi Ohori: A Polymorphic Record Calculus and Its Compilation, ACM Transactions on Programming Languages and
Systems, 17(6), 844--895, 1995.)


 

小林 直樹 氏(東北大学情報科学研究科)


授賞業績: 高階関数型プログラムの検証に関する研究
授賞理由:

小林氏は,Higher-Order Recursion Scheme (HORS) と呼ばれる,無限木を生成するための形式言語のモデル検査問題が決定可能であることを利用し,単純型付λ計算に対してのフロー解析,資源使用解析などの各種検証問題が,基底型の値が有限集合であれば決定可能であることを示した.また,HORSの新しいモデル検査アルゴリズムの考案と実際のプログラム検証器の実装を行い,最悪の場合の計算量が大きいにもかかわらず、実際のプログラムでは非常に高速に動作することを実証した.これは,形式言語理論とプログラミング言語の理論を組み合わせることにより,高階関数型プログラムの全自動検証手法を提案したものであり,新しい分野を切り拓く研究である.
2009年以降,ACM POPL (2009, 2010), IEEE LICS, ICALP などのトップカンファレンスで連続して論文が採択され,2011 年のLICS の招待講演を依頼されるなど,国際的に非常に高い評価を得ている.よって,日本ソフトウェア科学会は小林直樹氏に基礎研究賞を授与することとした.

出典:
Naoki Kobayashi: Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 416--428, 2009.