Mechanized formalization of formal tree languages in proof assistants

2016 Fiscal Year Final Research Report

• 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
• 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.

Free Research Field

情報学基礎