中野研究室 [中野研究室]

この文書は読取専用です。文書のソースを閲覧することは可能ですが、変更はできません。もし変更したい場合は管理者に連絡してください。
~~Title: 中野研究室 ~~

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

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

==== プログラミング言語処理系 ====

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

==== 関数型プログラミング ====

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

==== プログラム検証 ====

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

==== プログラム変換 ====

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

==== 形式言語理論 ====

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

==== 双方向変換 ====

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

==== プログラミング言語意味論 ====

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

==== 論理学 ====

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

===== 研究室学生の対外発表 =====
  * 2024年03月 **伊藤耀**さんが国内研究集会[[https://sites.google.com/faculty.gs.chiba-u.jp/cscat2024/home|CSCAT 2024]]で登壇発表しました．
  * 2024年03月 **上西真由**さん，**菅野直孝**さん，**中村 卓武**さん，**野木知優**さん，**齋藤佑貴**さんが国内研究集会[[https://jssst-ppl.org/workshop/2024/program|PPL 2024]]でポスター発表しました．
  * 2024年03月 **橋場慧志**さんが国内研究集会[[https://jssst-ppl.org/workshop/2024/program|PPL 2024]]で登壇発表しました．
  * 2023年03月 **菅野直孝**さん，**伊藤耀**さん，**野木知優**さんが国内研究集会[[https://jssst-ppl.org/workshop/2023/program|PPL 2023]]でポスター発表しました．
  * 2022年03月 **芳賀勇太**さん，**宮坂優介**さん，**上西真由**さんが国内研究集会[[https://jssst-ppl.org/workshop/2022/program|PPL 2022]]でポスター発表しました．
  * 2021年09月 **佐藤光**さんが国内学会[[https://jssst2021.wordpress.com/program/#ppl4_2|ソフトウェア科学会大会 2021]]で登壇発表しました．
  * 2021年03月 **今津徹大**さん，**佐藤光**さんが国内研究集会[[https://easychair.org/smart-program/PPL2021/|PPL 2021]]でポスター発表しました．
  * 2020年03月 **西山舜**さんが国内研究集会[[https://easychair.org/smart-program/PPL2020/|PPL 2020]]でポスター発表しました．
  * **2019年09月 高橋祐多さんの下記のCIAA 2019の論文がSpecial Issueに選出されました．**
    * **[[https://doi.org/10.1016/j.tcs.2020.12.033|これを受け更に発展させた論文]]が雑誌[[https://www.journals.elsevier.com/theoretical-computer-science|TCS]]に受理されました．**
  * **2019年04月 高橋祐多さんの[[https://doi.org/10.1007/978-3-030-23679-3_19|修士論文に基づいた論文]]が国際会議[[https://im.saske.sk/ciaa2019/|CIAA 2019]]に受理され，Slovakiaにて登壇発表しました．**
  * 2019年03月 **高橋祐多**さんが国内研究集会[[https://jssst-ppl.org/workshop/2019/program.html|PPL 2019]]で登壇発表しました．
  * 2019年03月 **小澤祐也**さんが国内研究集会[[https://jssst-ppl.org/workshop/2019/program.html|PPL 2019]]でポスター発表しました．
  * 2018年11月 **小澤祐也**さんが国内研究集会[[https://ksk.github.io/tpp2018/|TPP 2018]]で登壇発表しました．
  * 2018年10月 **阿部和敬**さん，**小澤祐也**さん，**高橋祐多**さんが国内研究集会[[https://sigpro.ipsj.or.jp/pro2018-3/program/|PRO 2018(3)]]で登壇発表しました．

===== 出版論文 =====
^ 論文DL                                                  ^ 出版年  ^ 論文タイトル                                                                           ^ 著者名                                                                                                                  ^ 雑誌・会議名                                                                                                                    ^
| [[https://doi.org/10.1145/3632855|doi]]                 | 2024    | Enriched Presheaf Model of Quantum FPC                                                 | Takeshi Tsukada and Kazuyuki Asada                                                                                      | [[https://popl24.sigplan.org/|Principles of Programming Languages (POPL 2024)]]                                                 |
| [[https://doi.org/10.1007/978-3-031-37709-9_3|doi]]     | 2023    | Compositional Probabilistic Model Checking with String Diagrams of MDPs                | Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo                                                      | [[http://www.i-cav.org/2023/|Computer Aided Verification (CAV 2023)]]                                                           |
| [[https://doi.org/10.1007/978-3-031-19135-0_8|doi]]     | 2022    | On Higher-Order Reachability Games vs May Reachability                                 | Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi                                                                       | [[https://rp2022.mpi-sws.org/index.html|Reachability Problems (RP 2022)]]                                                       |
| [[https://dl.acm.org/doi/10.1145/3531130.3533373|doi]]  | 2022    | Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings  | Takeshi Tsukada and Kazuyuki Asada                                                                                      | [[https://lics.siglog.org/lics22/index.php|Logic in Computer Science (LICS 2022)]]                                              |
| [[https://doi.org/10.4204/EPTCS.351.17|doi]]            | 2021    | A Compositional Approach to Parity Games                                               | Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo                                                      | [[https://www.coalg.org/calco-mfps2021/|Mathematical Foundations of Programming Semantics (MFPS 2021)]]                         |
| [[https://doi.org/10.4230/LIPIcs.MFCS.2021.79|doi]]     | 2021    | Idempotent Turing Machines                                                             | Keisuke Nakano                                                                                                          | [[https://compose.ioc.ee/mfcs/|Mathematical Foundations of Computer Science (MFCS 2021)]]                                       |
| [[https://doi.org/10.1007/978-3-030-79837-6_11|doi]]    | 2021    | A Tangled Web of 12 Lens Laws                                                          | Keisuke Nakano                                                                                                          | [[https://reversible-computation-2021.github.io/|Reversible Computation (RC 2021)]]                                             |
| [[https://doi.org/10.1007/978-3-030-52482-1_3|doi]]     | 2020    | Involutory Turing Machines                                                             | Keisuke Nakano                                                                                                          | [[https://reversible-computation-2020.github.io/|Reversible Computation (RC 2020)]]                                             |
| [[https://doi.org/10.23638/LMCS-16(2:8)2020|doi]]       | 2020    | On properties of B-terms                                                               | Mirai Ikebuchi and Keisuke Nakano                                                                                       | Logical Methods in Computer Science                                                                                             |
| [[https://doi.org/10.4230/LIPIcs.FSCD.2020.22|doi]]     | 2020    | Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars   | Kazuyuki Asada and Naoki Kobayashi                                                                                      | [[https://fscd2020.org/|Formal Structures for Computation and Deduction (FSCD 2020)]]                                           |
| [[https://doi.org/10.4230/LIPIcs.FSCD.2020.21|doi]]     | 2020    | On Average-Case Hardness of Higher-Order Model Checking                                | Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada                                    | [[https://fscd2020.org/|Formal Structures for Computation and Deduction (FSCD 2020)]]                                           |
| [[https://doi.org/10.1016/j.tcs.2020.12.033|doi]]       | 2020    | Streaming Ranked-Tree-to-String Transducers                                            | Yuta Takahashi, Kazuyuki Asada, and Keisuke Nakano                                                                      | Theoretical Computer Science                                                                                                    |
| [[https://doi.org/10.1007/978-3-030-23679-3_19|doi]]    | 2019    | Streaming Ranked-Tree-to-String Transducers                                            | Yuta Takahashi, Kazuyuki Asada, and Keisuke Nakano                                                                      | [[https://im.saske.sk/ciaa2019/|Implementation and Application of Automata (CIAA 2019)]]                                        |
| [[https://doi.org/10.1109/BIGCOMP.2019.8679145|doi]]    | 2019    | Toward BX-based Architecture for Controlling and Sharing Distributed Data              | Yasunori Ishihara, Hiroyuki Kato, Keisuke Nakano, Makoto Onizuka, and Yuya Sasaki                                       | [[http://www.prg.nii.ac.jp/projects/biscuits/second-workshop/|Software Foundations for Data Interoperability (SFDI 2019)]]      |
| [[https://doi.org/10.1109/BIGCOMP.2019.8679236|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  | [[http://www.prg.nii.ac.jp/projects/biscuits/second-workshop/|Software Foundations for Data Interoperability (SFDI 2019)]]      |
| [[https://doi.org/10.4230/LIPIcs.FSTTCS.2018.14|doi]]   | 2018    | Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered                         | Kazuyuki Asada and Naoki Kobayashi                                                                                      | [[https://www.fsttcs.org.in/archives/2018/|Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)]]  |
| [[https://doi.org/10.4230/LIPIcs.FSCD.2018.18|doi]]     | 2018    | On repetitive right application of B-terms                                             | Mirai Ikebuchi and Keisuke Nakano                                                                                       | [[https://www.cs.le.ac.uk/events/fscd2018/|Formal Structures for Computation and Deduction (FSCD 2018)]]                        |
| [[https://doi.org/10.11309/jssst.35.52|doi]]            | 2018    | 木から文字列への決定性トップダウン変換の等価性判定アルゴリズムの実用性について         | 高橋 祐多, 中野 圭介                                                                                                    | コンピュータ ソフトウェア                                                                                                       |

===== メンバー =====

^ 役職          ^ 名前                                                 ^ Name                ^ Email (+ <-> @)                      ^
| 教授          | [[https://www.riec.tohoku.ac.jp/~ksk/|中野 圭介]]    | NAKANO Keisuke      | ksk + riec.tohoku.ac.jp              |
| 助教          | [[https://www.riec.tohoku.ac.jp/~asada/|浅田 和之]]  | ASADA Kazuyuki      | asada + riec.tohoku.ac.jp            |
| :::           | [[https://kentaro-kikuchi.github.io/|菊池 健太郎]]   | 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       | Julia Plotnikova                                     | Julia Plotnikova  | plotnikova.julia.s6 + 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年：上西 真由（修士），菅野 直孝（修士），橋場 慧志（学士）
  * 2023年：芳賀 勇太（修士），宮坂 優介（修士），石鉢 健太（学士）
  * 2022年：佐藤 光（修士）
  * 2021年：今津 徹大（修士）
  * 2020年：西山 舜（修士），眞田 耕太（学士）
  * 2019年：阿部 和敬（修士），小澤 祐也（修士），高橋 祐多（修士）
===== リンク =====
  * [[https://www.tohoku.ac.jp/|東北大学]]
  * [[http://www.riec.tohoku.ac.jp/|東北大学 電気通信研究所]]
  * [[https://ipl.cs.uec.ac.jp/|電気通信大学 岩崎研究室]]
  * [[http://research.nii.ac.jp/~hu/|国立情報学研究所 胡研究室]]
  * [[http://takeichi.ipl-lab.org/|東京大学 武市研究室跡]]
  * [[internal:start]]