中野研究室

中野研究室では，プログラミングに関連するさまざまな研究を行っています．
主に以下のようなトピックを研究テーマとしています．

「プログラミング言語」と言われて皆さんがイメージするのはどのような言語でしょう？ C, Java, それとも他の言語でしょうか． 世の中には何千ものプログラミング言語が存在すると言われています． こんなにたくさんの言語が存在する理由は， 目的や用途によって適した言語が異なるためです． プログラミング言語処理系の研究では， 従来のプログラミング言語に手を加えて目的に適した機能を追加したり， 用途に合った小さなプログラミング言語を自ら開発したりすることを実現しています． 既存のコンパイラの修正による実行プログラムの高速化にも取り組んでいます．

近年，関数型プログラミングとよばれるデータフローを明確にした プログラミングスタイルが話題となっています． 複数のビジネス誌に特集として取り上げられるなど， 企業からの注目も高い研究分野です． 実際，Google の検索エンジンで利用されていることで有名な MapReduce は 関数型プログラミングのアイデアから生まれたものであり， 膨大なメッセージの効率的な処理が必要な Twitter の実装も Scala という言語を用いて関数型プログラミングによって実現されています． 関数型プログラミングについての研究では， より使いやすくするための解決方法を提案したり， 実行効率を向上させるための新たな実装を開発したりしています．

皆さんは，講義や演習でプログラミングをするとき， 正しく動作することをどのように確認しているでしょうか． いろいろな入力でテスト実行してみたり， プログラムの途中に print 命令を挿入して途中経過を観察したりしていませんか？ プログラムの検証は， 「実行せずにプログラムの性質を知る」ための研究です． 基本的にテスト実行では限られた数の入力しかテストできないため， 本当に正しく動くかは保証されません． 本研究では，全ての入力に対して正しく動作するということを数学的な手法で証明しているため， より正確にプログラムの性質を知ることが可能になります．

一般的に「短絡的に書いたプログラムは，読みやすい一方で効率が悪く， 効率を良くするために工夫して書いたプログラムは， 読みにくい上にデバッグもしにくい」というジレンマがあります． 効率を意識したプログラムは，複雑なアルゴリズムを用いているため， ちょっとした問題設定の変更に対してどのように修正すべきかは単純ではありません． プログラム変換の研究では， 短絡的に書いたプログラムを 効率のよいプログラムに自動変換することを実現します． これにより，読みやすく修正もしやすいプログラミングのもとで， 効率の良い実行プログラムを得ることができます．

講義などでオートマトンや形式文法などを勉強したことがあると思いますが， 形式言語理論はそれらを深く探求する分野です． 講義では何のために役に立つか分からないまま学習していたかもしれませんが， プログラミング言語の分野では非常に重要なテーマです． ここで挙げている研究テーマの中では最も理論的で数学的な素養が必要になりますが， プログラムの検証から効率化にいたるまで， さまざまなプログラミングの分野で応用可能な実用的な研究の1つです．

双方向変換系は，データベースを安全かつ効率的に更新するための研究です． データベースから必要な情報だけを抽出して見やすく整形したものをビューとよびますが， このビューの内容を修正することで， その修正をデータベース側に反映してしまおうというのが双方向変換のアイデアです． ここで「必要な情報を抽出して見やすく整形する」 という部分を一つのプログラムで記述されていると考えると， そのプログラムは， データベースを入力としてビューを出力するものであると見なせます． したがって，ビュー側の修正をデータベースに反映するためには， このプログラムを逆方向に実行する必要があるわけです． 双方向変換の研究では， この逆方向の実行を自動化するための枠組みを対象にして， 実現するための理論やその実用化に取り組んでいます．

プログラミング言語意味論は主に表示的意味論・操作的意味論・公理的意味論からなっています． 表示的意味論はプログラミング言語の構成要素（型やプログラムなど）を数学的構造（ある種の空間や関数など，あるいは別の言語）に「表示（解釈）」し，プログラミング言語の構造や性質を数学的に解明します． 表示的意味論の一種として圏論的意味論があり，抽象的な視点からプログラミング言語を研究するのに役立ちます． 操作的意味論はプログラムの手続き的な意味を定めるもので，この操作的意味論と表示的意味論の一致を示すことで，両意味論の正当性を高めます． 公理的意味論はプログラムのための論理体系を構築し，プログラムに関する推論を形式的に行う手段を提供します． これら意味論は各種定理により互いに関係を持ち，一体となって研究されます． その主な応用として，「プログラミング言語の設計」と「プログラミング言語の検証体系・推論体系の開発」の2つが挙げられます． プログラミング言語意味論は，上記に挙げられた研究室の各テーマの基礎理論としても重要です．

計算可能性理論やプログラミング言語理論の研究は形式論理学と深い繋がりがあり，当研究室も形式論理学の研究も行っています． 形式論理学のなかでも数学の論理学的基礎を研究する数学基礎論は，伝統的には再帰理論・証明論・モデル理論・集合論に分かれ， いずれも計算機科学と関係の深い分野ですが，なかでも証明論と計算体系の間にはCurry-Howard対応という1対1の関係が知られており， 両者は不可分の関係にあります． 直観主義命題論理が関数型言語のモデルである型付ラムダ計算と対応し，古典命題論理が第一級継続計算という大域的制御構造を持つ型付ラムダ計算と対応します． また上記のプログラミング言語意味論では，再帰理論的手法・モデル理論的手法・集合論的手法が用いられることもあります． 型理論も論理学と計算機科学の学際領域で活発に研究されているものです． 当研究室でも，その基礎理論からCoqなどの定理証明支援系まで研究を行っています． また論理学に近い数学の技術として圏論というものがあり，我々の研究でもテーマによっては用いられています．

• 2023年03月 菅野直孝さん，伊藤耀さん，野木知優さんが国内研究集会PPL 2023でポスター発表しました．
• 2022年03月 芳賀勇太さん，宮坂優介さん，上西真由さんが国内研究集会PPL 2022でポスター発表しました．
• 2021年09月 佐藤光さんが国内学会ソフトウェア科学会大会 2021で登壇発表しました．
• 2021年03月 今津徹大さん，佐藤光さんが国内研究集会PPL 2021でポスター発表しました．
• 2020年03月 西山舜さんが国内研究集会PPL 2020でポスター発表しました．
• 2019年09月 高橋祐多さんの下記のCIAA 2019の論文がSpecial Issueに選出されました．
  • これを受け更に発展させた論文が雑誌TCSに受理されました．
• 2019年04月 高橋祐多さんの修士論文に基づいた論文が国際会議CIAA 2019に受理され，Slovakiaにて登壇発表しました．
• 2019年03月 高橋祐多さんが国内研究集会PPL 2019で登壇発表しました．
• 2019年03月 小澤祐也さんが国内研究集会PPL 2019でポスター発表しました．
• 2018年11月 小澤祐也さんが国内研究集会TPP 2018で登壇発表しました．
• 2018年10月 阿部和敬さん，小澤祐也さん，高橋祐多さんが国内研究集会PRO 2018(3)で登壇発表しました．

OB：

• 2023年：芳賀 勇太（修士），宮坂 優介（修士），石鉢 健太（学士）
• 2022年：佐藤 光（修士）
• 2021年：今津 徹大（修士）
• 2020年：西山 舜（修士），眞田 耕太（学士）
• 2019年：阿部 和敬（修士），小澤 祐也（修士），高橋 祐多（修士）

• 東北大学
• 東北大学 電気通信研究所
• 電気通信大学 岩崎研究室
• 国立情報学研究所 胡研究室
• 東京大学 武市研究室跡
• 内部ページ