Abstraction preservation and subtyping in distributed languages

In most programming languages, type abstraction is guaranteed by syntactic scoping in a single program, but is not preserved by mar-shalling during distributed communication. A solution is to gener-ate hash types at compile time that consist of a fingerprint of the source code implementing the data type. These hash types can be tupled with a marshalled value and compared efficiently at unmar-shall time to guarantee abstraction safety. In this paper, we extend a core calculus of ML-like modules, functions, distributed com-munication, and hash types, to integrate structural subtyping, user-declared subtyping between abstract types, and bounded existen-tial types. Our semantics makes two contributions: (1) the explicit tracking of the interaction between abstraction boundaries and sub-typing; (2) support for user-declared module upgrades with propa-gation of the resulting subhashing relation throughout the network during communication. We prove type preservation, progress, de-terminacy, and erasure for our system