小林　直樹　君

[対象業績]　「高階モデル検査に関する研究およびIFIPに対する貢献」

1991年3月東京大学理学部情報科学科卒業. 1993年3月東京大学大学院学系研究科修士課程修了. 1993年11月東京大学大学院理学系研究科助手. 1996年4月東京大学大学院学系研究科博士（理学）取得. 1996年6月東京大学大学院理学系研究科講師. 平成13年1月東京工業大学大学院情報理工学研究科助教授. 2004年10月東北大学大学院情報科学研究科教授. 2012年4月東京大学大学院情報理工学系研究科教授. 現在に至る. 

小林直樹氏は, プログラミング言語の基礎理論, 特にプログラム解析・検証に関して数々の先駆的研究を行ってきた. 特に, 1990年代後半から2000年代にかけて行った型に基づく並行プログラムの自動解析手法の発明, 2009年から行った高階モデル検査に基づく新しいプログラム自動検証手法の発明は, 革新性, 斬新性が高い, 極めて重要な成果である. また, 2009年1月から9年の長期にわたってIFIP TC1日本代表を務め, 情報処理学会およびIFIPに貢献するとともに, プログラミング言語および理論計算機科学分野の国際的発展と日本のプレゼンス向上に貢献した.