Type Inference of Object-Oriented Programs with Exceptions Based on Term Rewriting

基于术语重写的面向对象程序异常类型推断

• 批准号: 16300005
• 负责人: SAKABE Toshiki
• 金额: $ 3.86万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2004
• 资助国家: 日本
• 起止时间: 2004 至 2007
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-16300005/
• 关键词: Object-Oriented Program; Exception Handling; Secrecy; Type Inference; Term Rewriting System; 通信エラー; 逆計算

The purpose of this research is to develop static verification methods for safeness of programs by applying rich results obtained so far on term rewriting systems, and also to create new research topics of term rewriting systems.There are three main topics of this research : safeness of programs, termination of term rewriting systems and program transformations. (1) As for safeness of programs, we have developed a type system for verifying secrecy of object-oriented programs with exceptions, a type system for checking communication errors in programs of Join JAVA, which is a JAVA combined with Join Calculus, and also methods for verifying safeness of programs of Spi Calculus and Petri Net. (2) For termination of term rewriting systems, a result on decidability of termination has been obtained. Sufficient conditions for termination of higher order term rewriting systems have been obtained by extending the dependency pair method. (3) In the research of program transformation, an inversion procedure for term rewriting systems has been developed. Being triggered by the work on program safeness we have given a sufficient condition for termination of a procedure transforming systems of eqations to systems of rewriting rules, where this transformation is used in the secrecy verification procedure for the applied pi calculus.

本研究的目的是利用已有的关于项重写系统的丰富成果，开发程序安全性的静态验证方法，并为项重写系统创造新的研究课题。本文主要研究三个主题：程序的安全性、术语重写系统的终止和程序转换。(1)在程序的安全性方面，我们开发了面向对象的异常程序的保密性校验类型系统，Join JAVA程序通信错误校验类型系统，它是一个结合了Join Calculus的JAVA程序，以及Spi Calculus和Petri Net程序的安全性校验方法。(2)对于项改写系统的终止，得到了终止的可判定性的结果。通过对依赖对方法的扩展，得到了高阶项重写系统终止的充分条件。(3)在程序变换的研究中，提出了一种项重写系统的反演方法。在程序安全工作的启发下，我们给出了将方程系统转换为重写规则系统的过程终止的充分条件，该转换用于应用pi微积分的保密验证过程。

项目成果

Higher-Order Knuth-Bendix Procedure and its Applications

高阶 Knuth-Bendix 过程及其应用

• 发表时间: 2004
• 期刊: LA-Symposium 2004(Summer)
• 作者: K.Kusakari;Y.Chiba
• 通讯作者: Y.Chiba

Enhancing Dependency Pair Method by Strong Computability in Simply-Typed Term Rewriting

通过简单类型术语重写中的强可计算性增强依赖对方法

• 发表时间: 2007
• 期刊: Applicable Algebra in Engineering, Communica-tion and Computing 18
• 作者: Keiichirou Kusakari;Masahiko Sakai
• 通讯作者: Masahiko Sakai

Convergent Term Rewriting Systems for Inverse Computation of Injec-tive Fhnctions

单射函数逆计算的收敛项重写系统

• 发表时间: 2007
• 期刊: Proc. of the 9th International Workshop on Ter-mination
• 作者: Naoki Nishida;Masahiko Sakai;and Terutoshi Kato
• 通讯作者: and Terutoshi Kato

Static Dependency Pair Method for Proving Termination of Higher-Order Rewriting Systems

证明高阶重写系统终止的静态依赖对方法

• 发表时间: 2007
• 期刊: 電子情報通信学会技術研究報告(SS2007-61) 107
• 作者: Kiichirou Kusakari;Yasuo Iso-gai;Masahiko Sakai;Toshiki Sakabe Naoki Nishida
• 通讯作者: Toshiki Sakabe Naoki Nishida

Usable Rules and Labeling Product-Typed Terms for De-pendency Pair Method in Simply-Typed Term Rewriting Systems

简单类型术语重写系统中依赖对方法的可用规则和标签产品类型术语

• 发表时间: 2007
• 期刊: IEICE Transactions on Information and Systems Vol.J90-D, No.4(Refereed)
• 作者: Takahiro;Sakurai;Keiichirou;Kusakari;Masahiko;Sakai;Toshiki;Sakabe;Naoki;Nishida
• 通讯作者: Nishida