教員

研究室HP

https://www.ipl.riec.tohoku.ac.jp/dokuwiki//ja/start

研究活動

本研究室の究極的な目標は人間と計算機の間の隔たりを埋めることである。人間が計算機に命令を行う方法としてプログラムを記述する方法があるが、人間と計算機の思考には隔たりがある。人間に合わせた記述では実行効率が下がり計算機に負担がかかってしまい、計算機に合わせた記述では開発効率が下がり人間に負担がかかってしまう。そこで、人間に合わせた記述から計算機に合わせた記述を導く研究や、計算機に合わせた記述が人間の意図に沿っているかを証明する研究に取り組んでいる。

コンピューティング情報理論研究分野｜中野教授

研究テーマ

• 木変換および木オートマトンの基礎理論
• プログラム変換およびプログラム検証
• 定理証明支援系による各種理論の定式化
• 結合子論理に潜む計算の仕組みや現象の解明

本分野では、プログラムや計算を抽象化した構造について多くの成果を残している形式木言語理論を対象に研究を進めている。具体的には、木トランスデューサとよばれる木構造から木構造への変換に関する理論を精査し発展させることにより、効率的なプログラムを導出したり、プログラマが望む計算の性質を保証したりする枠組みの開発に取り組んでいる。また、定理証明支援系とよばれる計算機によって証明の正しさを検査するシステムを用いた研究も進めている。
また、プログラミング言語意味論の研究も行っている。上述の形式言語技術が目的に応じてプログラムの一定側面のみを抽象するのに対し、こちらの手法ではプログラムの本質的な意味を全て保持した抽象化を行い、それを数学的に分析することにより、対象となるプログラミング言語の本質を明らかにする。具体的には、表示的意味論・操作的意味論・公理的意味論・圏論的意味論などがあり、プログラミング言語の理論的設計や前述の形式言語理論の技術と組合せプログラム検証などに応用する。