HOME >  組織・研究分野 >  中野研究室

組織・研究分野

コンピューティング情報理論 [中野] 研究室

教員・職員

photo 教授 中野 圭介 (電気通信研究所) (写真)
助教 浅田 和之 (電気通信研究所)

プログラミングは,人間がコンピュータを自在に操るために最も確実な手段の一つである. しかしながら,人間の思考に合わせて記述したプログラムは,必ずしもコンピュータにとって実行しやすいものとは限らない. プログラムを効率よく実行するには,コンピュータの枠組みに合わせて複雑なプログラムを記述する必要がある. 本研究室では,このような「複雑であるが効率のよいプログラム」を「人間の思考に沿ったプログラム」から自動的に導出するプログラム変換や, 「効率のために複雑に記述されたプログラム」が人間の意図通りに動作することを保証するプログラム検証の研究に取り組んでいる.

コンピュータの扱う多くのデータは木構造として捉えることができ,それらを扱うプログラムは木構造変換と考えることができる. 形式木言語理論は木構造データやその変換を形式的に扱うためのものであり, 本研究室ではこの理論の結果を利用し,木構造を対象とするプログラムの効率化 (プログラム変換) や静的型検査 (プログラム検証) の実現を進めている. また,ある特定の形をした木構造変換であれば等価性判定が可能であることが知られており, これを応用すると2つのプログラムが同じ入力に対して必ず同じ出力を返すことを自動的に確認することもできる. さらに,定理証明支援系を用いてこれらの理論や既存の数学の形式化も進めている.

東北大学 電気・情報系
〒980-8579 仙台市青葉区荒巻字青葉 6-6-05
TEL : 022-795-7186(教務係)
Email :

mail