A Framework of Program Transformation by Templates with Automated Verification of the Correctness

2014 Fiscal Year Final Research Report

• Project/Area Number: 23700034
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Software
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: CHIBA Yuki 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (10509756)
• Project Period (FY): 2011-04-28 – 2015-03-31
• Keywords: プログラム変換 / 単純型付項書き換えシステム / パターンマッチング

Outline of Final Research Achievements

We construct a framework of program transformation by templates which can directly deal with higher order functions by extending the framework based on first order term rewriting. Simply typed term rewriting systems (STTRS, for short) are adopted as a computational model in our framework. In order to verify the correctness of transformation in our framework, we propose an equivalent transformation of STTRSs and give sufficient condition for guaranteeing the correctness of transformation based on the equivalent transformation.
We introduce the notion of STTRS patterns for creating transformation templates in our framework. STTRS pattern matching algorithm is proposed to analyze how to apply templates for transforming STTRSs.

Free Research Field

項書き換え