• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Fundamental research on algebraic meta-programming

Research Project

Project/Area Number 08458067
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionNagoya University

Principal Investigator

HAMAGUCHI Takeshi  Dept.of Engineering, Nagoya Univ., Research Associate, 工学研究科, 助手 (90273284)

Co-Investigator(Kenkyū-buntansha) KAWAGUCHI Nobuo  Dept.of Engineering, Nagoya Univ., Assistant Professor, 工学研究科, 助手 (10273286)
YUEN Shoji  Dept.of Engineering, Nagoya Univ., Assistant Professor, 工学研究科, 助手 (70230612)
AGUSA Kiyoshi  Dept.of Engineering, Nagoya Univ., Professor, 工学研究科, 教授 (90026360)
INAGAKI Yasuyoshi  Dept.of Engineering, Nagoya Univ., Professor, 工学研究科, 教授 (10023079)
SAKABE Toshiki  Dept.of Engineering, Nagoya Univ., Professor, 工学研究科, 教授 (60111829)
馮 速  名古屋大学, 工学部, 助手 (90262881)
Project Period (FY) 1996 – 1997
Project Status Completed (Fiscal Year 1997)
Budget Amount *help
¥7,800,000 (Direct Cost: ¥7,800,000)
Fiscal Year 1997: ¥1,200,000 (Direct Cost: ¥1,200,000)
Fiscal Year 1996: ¥6,600,000 (Direct Cost: ¥6,600,000)
Keywordsmeta computation / rewriting computation / term rewriting system / concurrent computation / verification / algebraic specification / inductive theory / cover set induction
Research Abstract

Technologies verifying whether a program works according to the specification is important for improvement of software reliability. Since it is impossible to verify programs completely automatically, a system verifying software interactively is expected.
On developing such a verificat ion system, the following merits will come by keeping specification language, programming language, verification language and system describing language in the same language. Programrs, werifiers, and verification system developers have to learn only one kind of language. This is a significant advantage, because they must learn more than three kind of languages if the languages are different.
The language covering all processes of software specification, implementation, verification and development of verification system (called meta language), should provide properties desirable as each language. In particular, it needs to be provided with a clear logic that is a basis of verification and provided with a function to operate programs and specifications, i.e.meta computation, as a development language of verification system. It is also provides an easy implementation of interactive control of verification processes.
Through these two years, we have examined confluence of dynamic term rewriting systems, a class of term rewriting systems in which the functional strategy is normalizing, strategy for overlapping term rewriting systems, and a method for efficient concurrent-execution of term rewriting systems and got several results.

Report

(3 results)
  • 1997 Annual Research Report   Final Research Report Summary
  • 1996 Annual Research Report
  • Research Products

    (26 results)

All Other

All Publications (26 results)

  • [Publications] N.Kawaguchi, T.Sakabe, Y.Inagaki: "Environment for Supporting Analysis,Verification and Transformation of Term Rewriting Systems" Proc.on AMAST'96,LNCS. 1101. 571-574 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] S.Feng, T.Sakabe, Y.Inagaki: "Confluence Property of Simple Frames in Dynamic Term Rewriting Calculus" IEICE Trans.on Information and Systems. E80-D,6. 625-645 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 結縁、坂部、稲垣: "正則な実時間通信プロセスに対するテスト擬順序の記号的特性化、" 電子情報通信学会論文誌. J80-D-1,6. 474-484 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 粕谷, 酒井, 山本, 阿草: "項集合書換え系とその合流性" 電子情報通信学会論文誌. J80-D-I,4. 325-334 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] 蜂巣、山本、濱口、阿草: "An Efficient Implementation of Term Rewriting System on a Distributed Memory Architecture" IEICE Trans.on Information and Systems. E80-D,4. 510-517 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] M.Sakai: "Left-Incompatible Term Rewriting Systems and Functional Strategy" IEICE Trans.on Information and Systems. E80-D,12. 1176-1182 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] N.Kawaguchi, T.Sakabe, Y.Inagaki: "Visual Support Methods for Analysis, Verification, and Transformation of Term Rewriting Systems" Computer Software. 13,1 (in Japanese). 23-36 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] N.Kawaguchi, T.Sakabe, Y.Inagaki: "Implementing Visualization of Term Rewriting Computation in Standard ML" IEE Transaction. 116-C,1 (in Japanese). 103-110 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] N.Kawaguchi, T.Sakabe, Y.Inagaki: "Environment for Supporting Analysis, Verification and Transformation of Term Rewriting Systems" Proc.on AMAST'96, LNCS. 1101. 571-574 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Y.Takahashi, M.Sakai, Y.Toyama: "On the Confluence Property of COnditional Term Rewriting Systems" IEICE Trans.on Information and Systems. J79-D-I,11 (in Japanese). 897-902 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] S.Feng, T.Sakabe, Y.Inagaki: "Confluence Property of Simple Frames in Dynamic Term Rewriting Calculus" IEICE Trans.on Information and Systems. E80-D,6. 625-645 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] S.Yuen, T.Sakabe, Y.Inagaki: "Symbolic Alternative Characterizations of Testing Preorders for Regular Real-Communicating Processes" IEICE Trans.on Information and Systems. J80-D-I,6 (in Japanese). 474-484 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] H.Kasuya, M.Sakai, S.Yamamoto, K.Agusa: "Term Set Rewriting Systems and their Confluent Property" IEICE Trans.on Information and Systems. J80-D-I,4 (in Japanese). 325-334 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Y.Hachisu, S.Yamamoto, T.Hamaguchi, K.Agusa: "An Efficient Implementation of Term Rewriting System on a Distributed Memory Architecture" IEICE Trans.on Information and Systems. E80-D,4. 510-517 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] M.Sakai: "Left-Incompatible Term Rewriting Systems and Functional Strategy" IEICE Trans.on Information and System. E80-D,12. 1176-1182 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] S.Feng, T.Sakabe, T.Inagaki: "Confluence Property of Simple Frames in Dynamic Term Rewriting Calculus" IEICE Trans.on Information and Systems. E80-D,6. 625-645 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 結縁、坂部、稲垣: "正則な実時間通信プロセスに対するテスト擬順序の記号的特性化、" 電子情報通信学会 論文誌. J80-D-I,6. 474-484 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 粕谷、酒井、山本、阿草: "項集合書換え系とその合流性" 電子情報通信学会 論文誌. J80-D-I,4. 325-334 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 峰巣、山本、濱口、阿草: "An Efficient Implementation of Term Rewriting System on a Distributed Memory Architecture" IEICE Trans.on Information and Systems. E80-D,4. 510-517 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] M.Sakai: "Left-Incompatible Term Rewriting Systems and Functional Strategy" IEICE Trans.on Information and System. E80-D,12. 1176-1182 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] Su Feng: "Confluence Property of Simple Frames in Dynamic Term Rewriting Calculus" To appear in IEICE Transaction on Information and Systems. (1997)

    • Related Report
      1996 Annual Research Report
  • [Publications] Nobuo Kawaguchi: "TERSE : A Visual Environment for Supporting Analysis,Verification and Transformation of Term Rewriting Systems" Proc.of AMAST'96 (LNCS 1101). 571-574 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 鈴木晃: "命令を並列に実行するCPUに対するSCCSによるコンパイラ" 信学技報. COMP96-14. 49-58 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 大崎博基: "プログラム理解のための依存関係表示ツール" ソフトウェア工学の基礎III 日本ソフトウェア科学会 FOSE'96. 34-41 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 木野和佳: "プログラム動作理解のための抽象実行系" ソフトウェア工学の基礎III 日本ソフトウェア科学会 FOSE'96. 98-101 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] Masahiko Sakai: "Semantics and Strong Sequentiality of Priority Term Rewriting System" Proc.of RTA'96 (LNCS 1103). 377-391 (1996)

    • Related Report
      1996 Annual Research Report

URL: 

Published: 1996-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi