ja:start

東北大学電気通信研究所 コンピューティング情報理論研究室

中野研究室

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

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

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

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

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

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

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

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

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

  • 2024年07月 中村卓武さんが国内研究集会第7回機械学習工学研究会で登壇発表し,学生優秀発表賞を受賞しました.
  • 2024年03月 伊藤耀さんが国内研究集会CSCAT 2024で登壇発表しました.
  • 2024年03月 上西真由さん,菅野直孝さん,中村卓武さん,野木知優さん,齋藤佑貴さんが国内研究集会PPL 2024でポスター発表しました.
  • 2024年03月 橋場慧志さんが国内研究集会PPL 2024で登壇発表しました.
  • 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に選出されました.
  • 2019年04月 高橋祐多さんの修士論文に基づいた論文が国際会議CIAA 2019に受理され,Slovakiaにて登壇発表しました.
  • 2019年03月 高橋祐多さんが国内研究集会PPL 2019で登壇発表しました.
  • 2019年03月 小澤祐也さんが国内研究集会PPL 2019でポスター発表しました.
  • 2018年11月 小澤祐也さんが国内研究集会TPP 2018で登壇発表しました.
  • 2018年10月 阿部和敬さん,小澤祐也さん,高橋祐多さんが国内研究集会PRO 2018(3)で登壇発表しました.
論文DL 出版年 論文タイトル 著者名 雑誌・会議名
doi 2024 Enriched Presheaf Model of Quantum FPC Takeshi Tsukada and Kazuyuki Asada Principles of Programming Languages (POPL 2024)
doi 2023 Compositional Probabilistic Model Checking with String Diagrams of MDPs Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo Computer Aided Verification (CAV 2023)
doi 2022 On Higher-Order Reachability Games vs May Reachability Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi Reachability Problems (RP 2022)
doi 2022 Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings Takeshi Tsukada and Kazuyuki Asada Logic in Computer Science (LICS 2022)
doi 2021 A Compositional Approach to Parity Games Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo Mathematical Foundations of Programming Semantics (MFPS 2021)
doi 2021 Idempotent Turing Machines Keisuke Nakano Mathematical Foundations of Computer Science (MFCS 2021)
doi 2021 A Tangled Web of 12 Lens Laws Keisuke Nakano Reversible Computation (RC 2021)
doi 2020 Involutory Turing Machines Keisuke Nakano Reversible Computation (RC 2020)
doi 2020 On properties of B-terms Mirai Ikebuchi and Keisuke Nakano Logical Methods in Computer Science
doi 2020 Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars Kazuyuki Asada and Naoki Kobayashi Formal Structures for Computation and Deduction (FSCD 2020)
doi 2020 On Average-Case Hardness of Higher-Order Model Checking Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada Formal Structures for Computation and Deduction (FSCD 2020)
doi 2020 Streaming Ranked-Tree-to-String Transducers Yuta Takahashi, Kazuyuki Asada, and Keisuke Nakano Theoretical Computer Science
doi 2019 Streaming Ranked-Tree-to-String Transducers Yuta Takahashi, Kazuyuki Asada, and Keisuke Nakano Implementation and Application of Automata (CIAA 2019)
doi 2019 Toward BX-based Architecture for Controlling and Sharing Distributed Data Yasunori Ishihara, Hiroyuki Kato, Keisuke Nakano, Makoto Onizuka, and Yuya Sasaki Software Foundations for Data Interoperability (SFDI 2019)
doi 2019 Flexible framework for data integration and update propagation: system aspect Yasuhito Asano, Dennis-Florian Herr, Yasunori Ishihara, Hiroyuki Kato, Keisuke Nakano, Makoto Onizuka, and Yuya Sasaki Software Foundations for Data Interoperability (SFDI 2019)
doi 2018 Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered Kazuyuki Asada and Naoki Kobayashi Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)
doi 2018 On repetitive right application of B-terms Mirai Ikebuchi and Keisuke Nakano Formal Structures for Computation and Deduction (FSCD 2018)
doi 2018 木から文字列への決定性トップダウン変換の等価性判定アルゴリズムの実用性について 高橋 祐多, 中野 圭介 コンピュータ ソフトウェア
役職 名前 Name Email (+ ↔ @)
教授 中野 圭介 NAKANO Keisuke ksk + riec.tohoku.ac.jp
助教 浅田 和之 ASADA Kazuyuki asada + riec.tohoku.ac.jp
菊池 健太郎 KIKUCHI Kentaro kentaro.kikuchi + riec.tohoku.ac.jp
修士課程 伊藤 耀 ITO Yo yoito + riec.tohoku.ac.jp
中村 卓武 NAKAMURA Takumu takumu + riec.tohoku.ac.jp
野木 知優 NOGI Chihiro nogi + riec.tohoku.ac.jp
齋藤 佑貴 SAITO Yuki yuki1226 + riec.tohoku.ac.jp
許 兆恒 HUA Xiu-Heng Kevin xhua + riec.tohoku.ac.jp
佐藤 龍之介 SATO Ryunosuke sato.ryunosuke.q4 + dc.tohoku.ac.jp
COLABS Marie Marken Marie Marken marken.marie.magdalena.q6 + dc.tohoku.ac.jp
学士課程 小野寺 宏介 ONODERA Kosuke onodera.kosuke.s5 + dc.tohoku.ac.jp
中居 瑞希 Nakai Mizuki nakai.mizuki.q8 + dc.tohoku.ac.jp
長田 和樹 Nagata Kazuki nagata.kazuki.s1 + dc.tohoku.ac.jp

OB:

  • 2024年:上西 真由(修士),菅野 直孝(修士),橋場 慧志(学士),Julia Plotnikova(COLABS)
  • 2023年:芳賀 勇太(修士),宮坂 優介(修士),石鉢 健太(学士)
  • 2022年:佐藤 光(修士)
  • 2021年:今津 徹大(修士),Altermatt Jean-Marc Bastien(JYPE)
  • 2020年:西山 舜(修士),眞田 耕太(学士)
  • 2019年:阿部 和敬(修士),小澤 祐也(修士),高橋 祐多(修士)
  • ja/start.txt
  • 最終更新: 2024/10/01 14:53
  • by asada