コンピュータソフトウェア分野
プログラミング言語を主要テーマとして高効率・高信頼ソフトウェア構築のための理論と応用に関する研究を行っています．特に，型理論・モデル検査など，数理論理学に基づくプログラム検証技法の理論とその応用，そして関数プログラミングやオブジェクト指向プログラミングの考え方を生かした，抽象度が高い記述が可能なプログラミング言語の設計・開発に取り組んでいます．
教員
- 教授：五十嵐 淳
- 准教授：末永 幸平
- 助教：和賀 正樹
- 助教：池渕 未来
研究内容
プログラムの正しさを厳密に保証する
人間の書いたプログラムには誤りがつきものです．このような誤りはソフトウェアの誤動作につながり，大きな損害を引き起こすことがあります．本分野では，このような誤りがないことを保証するための，数学に基礎づけられた手法を研究しています．数学を基盤に置くことで，検証手法の信頼性が上がり，ひいてはプログラムの信頼性も上げることができます．
プログラムを書きやすくする
「抽象化」は物事の詳細を隠し本質をくくりだすことで人間の知的活動において重要な役割を果たしています．プログラミングにおいても例外ではなく，現在ほとんどのプログラミング言語が手続き，モジュール，クラスといった抽象化の機能を備えています．本分野ではアプリケーション分野に応じた適切な抽象化機構の開発とその理論や実装技術の研究を行っています．