UCAM-CL-TR-569: Global abstraction-safe marshalling with hash types

Publication announcement:

    Global abstraction-safe marshalling with hash types

    James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough

    Technical report UCAM-CL-TR-569, University of Cambridge,
    Computer Laboratory, June 2003, 86 pages.

This document is now available at

    http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-569.pdf

Abstract:

Type abstraction is a key feature of ML-like languages for writing large
programs. Marshalling is necessary for writing distributed programs,
exchanging values via network byte-streams or persistent stores. In this
paper we combine the two, developing compile-time and run-time semantics
for marshalling, that guarantee abstraction-safety between
separately-built programs.

We obtain a namespace for abstract types that is global, ie meaningful
between programs, by hashing module declarations. We examine the
scenarios in which values of abstract types are communicated from one
program to another, and ensure, by constructing hashes appropriately,
that the dynamic and static notions of type equality mirror each other.
We use singleton kinds to express abstraction in the static semantics;
abstraction is tracked in the dynamic semantics by coloured brackets.
These allow us to prove preservation, erasure, and coincidence results.
We argue that our proposal is a good basis for extensions to existing
ML-like languages, pragmatically straightforward for language users and
for implementors.

-- 
University of Cambridge, Computer Laboratory,
Technical Reports (ISSN 1476-2986)
http://www.cl.cam.ac.uk/TechReports/