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 *help |
¥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.
|
Report
(5 results)
Research Products
(14 results)
-
-
[Journal Article] Context-Preserving XQuery Fusion2014
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
Related Report
Peer Reviewed / Open Access
-
-
-
-
-
-
-
-
-
-
-
-
