HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Global abstraction-safe marshalling with hash types

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 report 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, i.e. 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.
Document type :
Complete list of metadata

Cited literature [150 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 6:37:53 PM
Last modification on : Thursday, February 3, 2022 - 11:18:26 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:35:32 PM


  • HAL Id : inria-00071732, version 1



James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough. Global abstraction-safe marshalling with hash types. [Research Report] RR-4851, INRIA. 2003. ⟨inria-00071732⟩



Record views


Files downloads