コンピューティング情報理論（中野）研究室は、2018年4月に発足しました。本研究室では、プログラミングやプログラミング言語に関する研究を行っています。

　プログラミングは人間が計算機に命令するための最も基本的な道具ですが、「人間にとっての考えやすさ」と「計算機にとっての処理のしやすさ」には大きな隔たりがあります。人間の思考に沿ったプログラムは可読性は高いものの、必ずしも計算機が効率よく処理できるとは限りません。一方、計算機の処理方法を考慮してプログラムを記述すれば時間や空間などの効率を上げることができますが、プログラムとしては複雑になり、デバッグや仕様変更による改良も困難になります。本研究室では、このような「人間」と「計算機」の間のギャップを埋める研究を進めています。

　具体的な研究テーマは「プログラム変換」と「プログラム検証」です。「プログラム変換」は、人間の思考に合わせた可読性の高いプログラムから、計算機の処理方法を考慮した効率のよいプログラムを自動生成する研究で、「プログラム検証」は、効率のために複雑に記述されたプログラムについて、その動作が与えられた仕様に沿ったものであるかを自動検査する研究です。本研究室では、これらの問題が木構造データ変換の数学的モデルの問題に対応していることに着目し、その理論の実用にむけた発展に取り組んでいます。このほか、我々の理論の正当性を固なものとするために定理証明支援系を用いた数学の形式化にも取り組んでいます。

　プログラミングに関する研究は現実世界での有用性が見えづらい分野ですが、多くの電子機器にはソフトウェアが搭載され、プログラムの効率化や検証が重要な役割を果たしています。本研究室は、このような「縁の下の力持ち」となる基盤づくりを目指しています。