小林 直樹（こばやし なおき、1968年 - ）は、日本の計算機科学者。東京大学大学院情報理工学系研究科教授。専門はプログラミング言語の基礎理論、型理論、プログラム解析、プログラム検証。とりわけ、並行プログラムの型システムおよび高階モデル検査に関する研究で知られる。

日本学術振興会賞、日本ソフトウェア科学会基礎研究賞などを受賞し、2020年には情報処理学会および日本ソフトウェア科学会のフェローに選出された。2025年度より日本ソフトウェア科学会理事長を務める。

経歴 1991年、東京大学理学部情報科学科を卒業。1993年、東京大学大学院理学系研究科情報科学専攻修士課程を修了し、同年、同研究科助手に就任。1996年に東京大学より博士（理学）の学位を取得し、同年、同研究科講師に就任した。

2001年に東京工業大学大学院情報理工学研究科助教授、2004年に東北大学大学院情報科学研究科教授を経て、2012年より東京大学大学院情報理工学系研究科教授。

国際会議LICS、ICALP、FSCDなどのプログラム委員長を歴任したほか、国際学術誌『Logical Methods in Computer Science』の編集委員などを務めている。2009年からは9年間にわたりIFIP TC1の日本代表を務めた。

研究 並行プログラムの型システム 1990年代後半から2000年代にかけて、並行計算におけるプログラム解析・検証のための型システムを研究した。通信チャネルの使用方法を型によって表現し、デッドロックやライブロックなど、並行プログラムの実行に関する性質を静的に解析する手法を発展させた。この研究に関する業績をうけ、2001年にIFIP TC2 Manfred Paul Award、2001年度に情報処理学会坂井記念特別賞を受賞している。

高階モデル検査とプログラム検証 2000年代末からは、関数型プログラミング言語などの高階関数を持つプログラムに対し、モデル検査を適用する研究を進めた。

2009年に発表した論文「Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs」では、高階関数型プログラムを、実行中に起こりうる事象の列を無限木として表す高階再帰スキーム（higher-order recursion scheme、HORS）に変換し、その木の性質をモデル検査することで元のプログラムを検証する手法を提案した。

また、高階再帰スキームのモデル検査のための型にもとづくアルゴリズムや、その実装に関する研究を行った。これらの成果をうけ、2010年度日本ソフトウェア科学会基礎研究賞を受賞している。

現在、高階不動点論理（higher-order fixpoint logic、HFL）を用いたモデル検査とプログラム検証などの研究を行っている。

主な受賞歴 2001年 - IFIP TC2 Manfred Paul Award。 2001年度 - 情報処理学会坂井記念特別賞。「並行プログラムの検証・解析のための型システムに関する研究」。 2003年 - 日本IBM科学賞。 2006年 - 文部科学大臣表彰若手科学者賞。 2008年度 - 第5回日本学術振興会賞。「ソフトウェア検証のための型理論」。授賞式は2009年3月に行われた。 2010年度 - 日本ソフトウェア科学会基礎研究賞。「高階関数型プログラムの検証に関する研究」。 2014年 - ETAPS 2014 EATCS Best Paper Award。稲葉一浩、塚田武志との共著論文「Unsafe Order-2 Tree Languages are Context-Sensitive」に対する受賞。 2020年 - 情報処理学会フェロー。「高階モデル検査に関する研究およびIFIPに対する貢献」。 2020年 - 日本ソフトウェア科学会フェロー。 2025年 - ETAPS 2025 Distinguished Paper Award。山田梨沙、酒寄健、佐藤亮介との共著論文「On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic」に対する受賞。

主な論文 Kobayashi, Naoki (2002). "A Type System for Lock-Free Processes". Information and Computation, 177(2), 122–159. Kobayashi, Naoki (2009). "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, 416–428. Kobayashi, Naoki; Inaba, Kazuhiro; Tsukada, Takeshi (2014). "Unsafe Order-2 Tree Languages are Context-Sensitive". Foundations of Software Science and Computation Structures (FoSSaCS 2014), 149–163. Yamada, Risa; Kobayashi, Naoki; Sakayori, Ken; Sato, Ryosuke (2025). "On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic". Programming Languages and Systems (ESOP 2025), 402–428.

脚注

外部リンク 小林直樹 - 東京大学 小林直樹 - 東京大学研究者紹介 小林直樹 - J-GLOBAL