定理証明支援系による形式木言語理論の定式化

• 研究課題/領域番号: 25730002
• 研究種目: 若手研究(B)
• 配分区分: 基金
• 研究分野: 情報学基礎理論
• 研究機関: 電気通信大学
• 研究代表者: 中野 圭介 電気通信大学, 大学院情報理工学研究科, 准教授 (30505839)
• 研究期間 (年度): 2013-04-01 – 2017-03-31
• 研究課題ステータス: 完了 (2016年度)
• 配分額: 3,380千円 (直接経費: 2,600千円、間接経費: 780千円); 2016年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2015年度: 780千円 (直接経費: 600千円、間接経費: 180千円); 2014年度: 780千円 (直接経費: 600千円、間接経費: 180千円); 2013年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
• キーワード: 形式言語理論 / 定理証明支援系 / 木トランスデューサ / 形式木言語理論 / 木オートマトン / 構造化文書 / 木トランスデューサ理論

研究成果の概要

木構造データから木構造データへ変換するモデルである木トランスデューサ理論は，プログラミング言語理論やデータベース理論において重要な役割を果たしており，1960年代から盛んに研究が行われている．本研究の目的は，この理論を計算機の上で定式化し，その中の定理に対して機械的に検査可能な形の厳密な証明を与えることである．この成果により，今後の同分野の着実な発展が期待され，さらに堅牢なソフトウェア開発への応用の基盤を提供することが可能となる．

研究成果

• [雑誌論文] XQuery Streaming by Forest Transducers (2015)
  • 著者名/発表者名: Shizuya Hakuta, Sebastian Maneth, Keisuke Nakano, and Hideya Iwasaki
  • 雑誌名: 30th IEEE International Conference on Data Engineering 巻: 30 ページ: 952-963
  • DOI: 10.1109/icde.2014.6816714
  • 査読あり / 謝辞記載あり
• [雑誌論文] Context-Preserving XQuery Fusion (2014)
  • 著者名/発表者名: Hiroyuki Kato, Soichiro Hidaka, Zhenjiang Hu, Keisuke Nakano and Yasunori Ishihara
  • 雑誌名: Mathematical Structures in Computer Science 巻: online 号: 4 ページ: 916-941
  • DOI: 10.1017/s096012951300008x
  • 査読あり / オープンアクセス
• [雑誌論文] XQuery Streaming by Forest Transducers (2014)
  • 著者名/発表者名: Shizuya Hakuta, Sebastian Maneth, Keisuke Nakano, and Hideya Iwasaki
  • 雑誌名: Proceedings of 30th International Conference on Data Engineering 巻: 30 ページ: 952-963
  • 査読あり
• [雑誌論文] Polynomial-Time Inverse Computation for Accumulative Functions with Multiple Data Traversals (2013)
  • 著者名/発表者名: Kazutaka Matsuda, Kazuhiro Inaba, Keisuke Nakano
  • 雑誌名: Higher-Order and Symbolic Computation 巻: Volume 25, Issue 1 号: 1 ページ: 3-38
  • DOI: 10.1007/s10990-013-9097-8
  • 査読あり / オープンアクセス
• [雑誌論文] Structural Recursion for Querying Ordered Graphs (2013)
  • 著者名/発表者名: Soichiro Hidaka, Kazuyuki Asada, Zhenjiang Hu, Hiroyuki Kato, and Keisuke Nakano
  • 雑誌名: Proceedings of 18th ACM SIGPLAN International Conference on Functional Programming 巻: 48 (9) ページ: 305-318
  • DOI: 10.1145/2500365.2500608
  • 査読あり
• [雑誌論文] A Parameterized Graph Transformation Calculus for Finite Graphs with Monadic Branches (2013)
  • 著者名/発表者名: Kazuyuki Asada, Soichiro Hidaka, Hiroyuki Kato, Zhenjiang Hu, and Keisuke Nakano
  • 雑誌名: Proceedings of 15th International Symposium on Principles and Practice of Declarative Programming 巻: 15 ページ: 73-84
  • DOI: 10.1145/2505879.2505903
  • 査読あり
• [学会発表] 属性文法合成による関数融合の実装 (2017)
  • 著者名/発表者名: 中川 涼太
  • 学会等名: 第19回プログラミングおよびプログラミング言語ワークショップ
  • 発表場所: 石和温泉 華やぎの章 (山梨県笛吹市)
  • 年月日: 2017-03-08
• [学会発表] 木から文字列への決定性トップダウン変換の等価性判定の実装 (2017)
  • 著者名/発表者名: 高橋 祐多
  • 学会等名: 第19回プログラミングおよびプログラミング言語ワークショップ
  • 発表場所: 石和温泉 華やぎの章 (山梨県笛吹市)
  • 年月日: 2017-03-08
• [学会発表] マクロ森トランスデューサの実用的な型検査に向けて (2017)
  • 著者名/発表者名: 阿部 和敬
  • 学会等名: 情報処理学会 第113回プログラミング研究発表会
  • 発表場所: 東京大学 (東京都文京区)
  • 年月日: 2017-03-04
• [学会発表] Bidirectional Certified Programming (2017)
  • 著者名/発表者名: Keisuke Nakano
  • 学会等名: Sixth International Workshop on Bidirectional Transformations
  • 発表場所: ウプサラ大学 (スウェーデン)
  • 国際学会
• [学会発表] On properties of B-terms (2016)
  • 著者名/発表者名: Keisuke Nakano
  • 学会等名: NJ Programming Languages and Systems Seminars
  • 発表場所: ペンシルバニア大学 (アメリカ)
  • 国際学会
• [学会発表] Grammatical Frameworkにおける語彙データの自動生成 (2015)
  • 著者名/発表者名: 渡邉秀隆, 中野圭介
  • 学会等名: 言語処理学会第21回年次大会
  • 発表場所: 京都大学
  • 年月日: 2015-03-16 – 2015-03-20
• [学会発表] XQuery Streaming by Forest Transducers (2014)
  • 著者名/発表者名: Keisuke Nakano
  • 学会等名: 30th International Conference on Data Engineering
  • 発表場所: Chicago, US
• [学会発表] XML stream processing based on tree transducer composition (2013)
  • 著者名/発表者名: Keisuke Nakano
  • 学会等名: Dagstuhl Seminar on Tree Transducers and Formal Methods
  • 発表場所: Dagstuhl, Germany
  • 招待講演