Modules, Abstract Types, and Distributed Versioning

Peter Sewell

Abstract:

In a wide-area distributed system it is often impractical to
synchronise software updates, so one must deal with many coexisting
versions.  This talk is about static typing support for modular wide-area
programming, modelling separate compilation/linking and execution of
programs that interact along typed channels.  Interaction may involve
communication of values of abstract types, so developers
need fine-grain versioning control of these types to support
interoperation of old and new code.

This is all made precise in terms of a second-class module system
with singleton kinds, with a novel operational semantics
for separate compilation/linking and execution.