Supported by the National Natural Science Foundation of China under Grant No.60173049 (国家自然科学基金); the Project of the Intel China Research Center (英特尔中国研究中心资助)
A Tag Type for Certifying Compilation of Java Program
In the area of language -based security, programs written in typed high-level languages need to be translated into those written in typed low-level languages. This work is not trivial when type dispatch constructs are involved and implemented with tag mechanism. This paper proposes a new type that can deal with a special type dispatch construct occurring in the interface invokation of Java. A low-level language with this type is able to efficiently implement the interface invokation. This implementation approach is adopted in a Just-In-Time compiler with a typed low-level language as a certifying language.