Abstra t types in distributed systems A partial translation of my Ph.D. dissertation

Consider a network of nodes running ML programs that ex hange data. How an data whi h has an abstra t type on one node be a epted on another node? A safe approa h is to treat abstra t types as distin t whenever they are dened on dierent nodes. However this is too restri tive in pra ti e, for example in the ommon ase where an abstra t type enfor es a semanti invariant. The main ontributions of this thesis are threefold: I dene a notion of hash of an abstra t type, whereby abstra t types that have the same hash are deemed ompatible; I give an operational semanti s for a module system that preserves types, in luding abstra t types; I also propose a new, more general module system that is well-suited to distributed appli ations. The hash of an abstra t type must re e t its intended semanti s, whi h is often not apparent from the program's ode. In pra ti e, two modules have the same hash if they have the same ode. Compound modules are ompatible when they are built from ompatible omponents. Existing operational semanti s for ML modules lose information as they erase abstra tion bound-aries. I use oloured bra kets to tra k the visibility of abstra t types. I study two al uli equipped with bra kets, a simply-typed lambda- al ulus and a ri h ML module al ulus. I use singleton signatures to keep tra k of not only type but also ode sharing, so that modul