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

点击翻译按钮获取中文摘要

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.