Hello Basile,

Pierre Weis <pierre.weis@inria.fr> writes:
...
> discussed in long the difference between writing then reading back
> values from a single executable and transferring data among unrelated
> programs
...

We (J.J. Leifer, G. Peskine, P. Sewell, K. Wansbrough) have worked on
a theory of type-safe marshalling for values of abstract types.  The
theory ensures type and abstraction safety when communicating between
separately built programs.  The idea is to calculate hashes
(fingerprints) of modules to generate type identifiers for abstract
types that are globally meaningful.  These hashes are then compared at
run-time in a dynamic check when unmarshalling.

The ICFP paper about this is ``Global abstraction-safe marshalling
with hash types'':

   http://pauillac.inria.fr/~leifer/research.html

There are limitations to the current theory (no polymorphism, no
functors, no reference cells, no versioning, no dynamic binding, ...)
that we are working to overcome.  Peskine is interested in the
polymorphism question and may try to do an implementation of safe
marshalling for Ocaml.  Some of Sewell's interns are also working on
implementations of various aspects of this in a toy ``mini'' Caml
language.

Basile, come visit us in MOSCOVA (Batiment 8) if you'll be in Rocq!

Best regards,
James
--
James LEIFER, MOSCOVA Project, INRIA Rocquencourt

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners