kirancodes.me
To Proof Maintenance & Beyond!

An interoperable calculus for external object access

Atsushi Ohori, Kiyoshi Yamatodani

Abstract

By extending an ML-style type system with record polymorphism, recursive type definition, and an ordering relation induced by field inclusion, it is possible to achieve seamless and type safe interoperability with an object-oriented language. Based on this observation, we define a polymorphic language that can directly access external objects and methods, and develop a type inference algorithm. This calculus enjoys the features of both higher-order programming with ML polymorphism and class-based object-oriented programming with dynamic method dispatch. To establish type safety, we define a sample object-oriented language with multiple inheritance as the target for interoperability, define an operational semantics of the calculus, and show that the type system is sound with respect to the operational semantics. These results have been implemented in our prototype interpretable language, which can access Java class files and other external resources.

Related papers