Mechanized formalization of formal tree languages in proof assistants

• Project/Area Number: 25730002
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Theory of informatics
• Research Institution: The University of Electro-Communications
• Principal Investigator: Keisuke Nakano 電気通信大学, 大学院情報理工学研究科, 准教授 (30505839)
• Project Period (FY): 2013-04-01 – 2017-03-31
• Project Status: Completed (Fiscal Year 2016)
• Budget Amount: ¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000); Fiscal Year 2016: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2015: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2014: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000); Fiscal Year 2013: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
• Keywords: 形式言語理論 / 定理証明支援系 / 木トランスデューサ / 形式木言語理論 / 木オートマトン / 構造化文書 / 木トランスデューサ理論

Outline of Final Research Achievements

The theory of tree transducers which models tree-to-tree transformations has been explored since 1960's and played an important role in theory of programming languages and databases. The goal of this project is to formalize the theory in computer where all proofs of theorems for tree transducers are mechanically ceritified. It enables us to easily and steadily expand the theory and apply it to development of robust softwares.

Research Products

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