教授中野 圭介

助教浅田 和之

中野 圭介

研究活動

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

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

本分野では、プログラムや計算を抽象化した構造について多くの成果を残している形式木言語理論を対象に研究を進めている。具体的には、木トランスデューサとよばれる木構造から木構造への変換に関する理論を精査し発展させることにより、効率的なプログラムを導出したり、プログラマが望む計算の性質を保証したりする枠組みの開発に取り組んでいる。また、定理証明支援系とよばれる計算機によって証明を検査するシステムを用いた研究も進めている。

研究テーマ

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