2011年12月07日寺内多智弘 准教授（情報システム学専攻）2011/4/1着任

米国のColumbia大学とUC Berkeleyで学位所得後、東北大学での助教を経て2011年に名古屋大学へ着任しました。同講座の結縁教授らと協力してプログラミング言語、特にプログラム解析・プログラム検証の研究を進めています。

• 

現代、コンピュータ及び様々な電子機器を動かしているのは「プログラム」です。携帯のアプリもカーナビも飛行機の制御システムもMacOS・Windowsなどのオペレーティングシステムも、全てプログラムで動いています。プログラムは人間の書くものであるため、プログラミングの間違いにより、コンピュータの誤作動・不具合に至ることがあります。

例えば、C言語のプログラムで、外部から入力として渡された値の範囲をチェックせず配列のインデックスとして使用すると、配列外のメモリのアクセスが起こり重大なシステムのエラーに繋がることがあります。プログラム解析・プログラム検証とは、こうしたプログラムの不具合(つまりバグ)の検出および防止を、プログラミング言語理論の技術を応用して行うというものです。プログラム解析・プログラム検証の手法は様々で、例えば、モデル検査・アブストラクトインタプリテーション・定理証明などがあり、複数の視点からの研究が進められています。

私が、現在特に力を入れて研究を進めている課題の1つである、型システムを用いた、関数を扱うプログラムの自動検証を紹介します。近年、モデル検査と呼ばれるプログラムの値や分岐を精密に扱える自動検証の研究の発展により、それまでの手法よりはるかに高度な精度の自動検証が可能になりました。しかし、プログラム検証はどの手法にも限界があり(最終的には決定不能な問題であるため)、モデル検査手法の弱点の1つとして関数を正確に扱うことが難しいということがありました。対して、型システムはプログラム中の関数を表現するのに適した枠組みです。例えば、

x:int->f:(y:{u:int|x <= u}->{u:int|u=x+y})->{u:int|u=2*x}

という型は整数xと「x以上の整数yを受け取りx+yを返す関数」fを引数として受け取り2*xを返すという関数を表現しています。この様に、型を用い簡潔かつ正確に関数の動作を表現するプログラム解析・プログラム検証を設計しています。
図は型システムを構築する「型付け規則」の1例です。