| Project/Area Number |
20500008
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SAKABE Toshiki 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
SAKAI Masahiko 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
NISHIDA Naoki 名古屋大学, 大学院・情報科学研究科, 助教 (00397449)
|
|---|
| Project Period (FY) |
2008 – 2011
|
| Project Status |
Completed (Fiscal Year 2011)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2011: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2010: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2009: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2008: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
|
|---|
| Keywords | 計算理論 / 関数プログラム / 再帰定義 / 停止性 / 静的依存対法 / 関数型言語 / 単純型付き書換え系 / 停止性証明 / 静的再帰構造 |
|---|
| Research Abstract |
The purpose of this research is to present a method for proving termination of higher-order functional programs, and to develop a termination prover based on the results. In particular, we investigate higher-order functions that are widely used in existing functional programs.
To such purpose, we present an extremely powerful method for proving termination, namely the static dependency pair method. The method combines the dependency pair method introduced for first-order rewrite systems with the notion of strong computability introduced for typed￥lambda-calculi. This method statically analysis a recursive structure of functional programs, and by solving suitable constraints generated by the analysis, we can prove termination. We also extend the argument filtering method and the notion of usable rules onto higher-order systems.
Moreover we produce a termination library of HOPSYS(Higher-Order Proving SYStem). Currently in order to release HOPSYS, we are preparing a manual and web user interface.
|
