TYPE-THEORETIC FOUNDATIONS FOR CONCURRENT OBJECT-ORIENTED PROGRAMMING

A number of attempts have been made to obtain type systems for object- oriented programming. The view that lies common is ''object-oriented p rogramming = lambda-calculus + record.'' Based on an analogous view '' concurrent object-oriented programming = concurrent calculus + record, '' we develop a static type system for concurrent object-oriented prog ramming. We choose our own Higher-Order ACL as a basic concurrent calc ulus, and show that a concurrent object-oriented language can be easil y encoded in the Higher-Order ACL extended with record operations. Sin ce Higher-Order ACL has a strong type system with a polymorphic type i nference mechanism, programs of the concurrent object-oriented languag e can be automatically type-checked by the encoding in Higher-Order AC L. Our approach can give clear accounts for complex mechanisms such as inheritance and method overriding within a simple framework.