Runtime Behavior of Conversion Interpretation of Subtyping

A programming language with subtyping can be translated into a language without subtyping by inserting conversion functions. Previous studies of this interpretation showed only the extensional correctness of the translation. We study runtime behavior of translated programs and show that this translation preserves execution time and stack space within a factor determined by the types in a program. Both the proofs on execution time and stack space are based on the method of logical relations where relations are extended with the factor of slowdown or increase of stack space.

• Type: Conference
• Year: 2001
• Where: IFL
• Authors: Yasuhiko Minamide
• Keywords: Execution Time, Formal Methods, IFL 2001, Stack Space, Translation Preserves Execution