東北大学大学院情報科学研究科 -- Graduate School of Information Sciences,Tohoku University --

住井英二郎准教授が第７回船井情報科学奨励賞を受賞


この度は第7回船井情報科学奨励賞をいただき、大変光栄に思います。これまでに厚くご指導いただいた小林直樹先生、Benjamin C. Pierce ペンシルバニア大学教授をはじめ、研究科および研究室の先生方ならびにメンバーの皆様への感謝の念にたえません。深くお礼を申し上げます。 ■業績概要　計算機ソフトウェアの不具合が多発し社会的問題となっている現在、プログラムの性質を網羅的・数理論理学的に検証することが重要となっています。通常の実行によるテストだけでは、有限（通常はごく一部）のケースしか検査することができないためです。しかし、一般に計算機プログラムの性質は、通常の数式以上に複雑です。たとえば、式Eに対して、E + Eという式を考えます。通常の数学であれば「E + E = 2E」等と言えますが、計算機プログラムでは破壊的代入や無限ループなど、 Eが「副作用」を持つ可能性があり、「E + E = 2E」が必ずしも成り立ちません。また、たとえばWebブラウザでソフトウェアをダウンロードするように、プログラムそのものを受け渡しする「高階プログラム」についても考えなければなりません。
		住井　英二郎　准教授
本研究では、代入やループ・再帰、オブジェクトやデータ抽象（すでにあるデータ構造を用いて新たなデータ構造を定義する機能）・多相型（任意の種類のデータに適用できる関数やデータ構造を定義する機能）、高階性・並列性などの現実的機能を有する幅広い計算モデルにおいて、「二つのプログラムが等しい」と言える初等的な必要十分条件を初めて与えました。この研究自体は基礎研究であり、今の世の中の計算機システムの不具合（バグ）が直ちに全て消えてなくなるようなものではありません。しかし、このような数理論理学的手法を研究することは、中長期的に「きちんと動くコンピュータ」を実現するためには必要不可欠であると考えています。

■関連論文 A Bisimulation for Type Abstraction and Recursion. Eijiro Sumii and Benjamin C. Pierce. Journal of the ACM, vol. 54, issue 5, article 26, pp. 1-43, October 2007. A Bisimulation for Dynamic Sealing. Eijiro Sumii and Benjamin C. Pierce. Theoretical Computer Science, vol. 375, issues 1-3, pp. 169-192, May 2007. Logical Relations for Encryption. Eijiro Sumii and Benjamin C. Pierce. Journal of Computer Security, vol. 11, no. 4, pp. 521-554, 2003.

住井 英二郎 准教授が 第７回船井情報科学奨励賞を受賞

住井英二郎准教授が
第７回船井情報科学奨励賞を受賞