| Project/Area Number |
24500012
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Gifu University (2013-2016)
Nagoya University (2012) |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
坂部 俊樹 名古屋大学, 情報科学研究科, 教授 (60111829)
|
|---|
| Co-Investigator(Renkei-kenkyūsha) |
SAKAI Masahiko 名古屋大学, 情報科学研究科, 教授 (50215597)
NISHIDA Naoki 名古屋大学, 情報科学研究科, 准教授 (00397449)
|
|---|
| Project Period (FY) |
2012-04-01 – 2017-03-31
|
| Project Status |
Completed (Fiscal Year 2016)
|
| Budget Amount *help |
¥5,070,000 (Direct Cost: ¥3,900,000、Indirect Cost: ¥1,170,000)
Fiscal Year 2016: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2015: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2014: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2013: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2012: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
|
|---|
| Keywords | 関数型プログラム / 停止性 / 再帰定義 / 情報基礎 / 関数プログラム |
|---|
| Outline of Final Research Achievements |
We formalize a rewriting model for functional programs, which can represent the notions of higher-order function, polymorphic type, algebraic data type, and functional abstraction with pattern. We extend the static dependency pair method, which proves the termination by analyzing a static recursive structure, onto this rewriting model. In order that this method gives full play to its ability, we also extend reduction orders, the argument filtering method, and the notion of usable rules, although present results do not handle functional abstraction with pattern. Since the syntax of our rewriting model is very close to SML-like functional programs, our result can expect the effective applicability to verification for existing functional programs.
|
