From: James Leifer <James.Leifer@inria.fr>
To: caml-list@inria.fr
Cc: basile@starynkevitch.net (Basile STARYNKEVITCH),
Peter Sewell <Peter.Sewell@cl.cam.ac.uk>,
Gilles.Peskine@inria.fr,
Keith Wansbrough <Keith.Wansbrough@cl.cam.ac.uk>
Subject: Re: [Caml-list] adding data persistency in Ocaml...
Date: Thu, 17 Jul 2003 09:56:34 +0200 [thread overview]
Message-ID: <r774r1llh71.fsf@brouilly.inria.fr> (raw)
In-Reply-To: <200307112205.AAA00369@pauillac.inria.fr>
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
next prev parent reply other threads:[~2003-07-17 7:56 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-07-10 11:33 Basile STARYNKEVITCH
2003-07-10 15:03 ` Erik Arneson
2003-07-11 22:05 ` Pierre Weis
2003-07-17 7:56 ` James Leifer [this message]
2003-07-13 9:54 ` John Max Skaller
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=r774r1llh71.fsf@brouilly.inria.fr \
--to=james.leifer@inria.fr \
--cc=Gilles.Peskine@inria.fr \
--cc=Keith.Wansbrough@cl.cam.ac.uk \
--cc=Peter.Sewell@cl.cam.ac.uk \
--cc=basile@starynkevitch.net \
--cc=caml-list@inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).