Type-safe distributed programming for OCaml

Existing ML-like languages guarantee type-safety, ensuring memty and protecting the invariants of abstract types, but only within single executions of single programs. Distributed programming is becoming ever more important, and should benefit even more from such guarantees. In previous work on theoretical calculi and the Acute prototype language we outlined techniques to provide them for simple languages. In this paper we put these ideas into practice, describing the HashCaml extension to the OCaml bytecode compiler, which supports type-safe and abstraction-safe marshalling, together with related naming constructs. Our contribution is threefold: (1) We show how to define globally meaningful runtime type names for key OCaml type constructs that were not covered in our previous work, dealing with the generativity issues involved: user-defined variant and record types, substructures, functors, arbitrary ascription, separate compilation, and external C functions. (2) We support marsha...

• Type: Conference
• Year: 2006
• Where: ML
• Authors: John Billings, Peter Sewell, Mark R. Shinwell, Rok Strnisa
• Keywords: Machine Learning, ML 2006, OCaml, Runtime Type Names, Value Restriction