topic.distributed_types.bib
@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c 'topic:"distributed_types" or topic:"distributed_types_and_update"' -ob topic.distributed_types.bib sewellbib2.bib}}
@techreport{Sew00,
author = {Peter Sewell},
title = {Modules, Abstract Types, and Distributed Versioning},
institution = {University of Cambridge},
year = {2000},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-506},
optaddress = {},
month = sep,
note = {46pp. },
optannote = {},
errata = {http://www.cl.cam.ac.uk/~pes20/versions-errata.txt},
ps = {http://www.cl.cam.ac.uk/~pes20/versions-tr.ps},
pdf = {http://www.cl.cam.ac.uk/~pes20/versions-tr.pdf},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-506.html},
abstract = {In a wide-area distributed system it is often impractical to synchronise software updates, so one must deal with many coexisting versions. We study static typing support for modular wide-area programming, modelling separate compilation/linking and execution of programs that interact along typed channels. Interaction may involve communication of values of abstract types; we provide the developer with fine-grain versioning control of these types to support interoperation of old and new code. The system makes use of a second-class module system with singleton kinds; we give a novel operational semantics for separate compilation/linking and execution and prove soundness.},
topic = {distributed_types}
}
@inproceedings{Sew01a,
author = {Peter Sewell},
title = {Modules, Abstract Types, and Distributed Versioning},
conf = {POPL 2001},
booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (London)},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {2001},
optorganization = {},
optpublisher = {},
optaddress = {},
month = jan,
pages = {236--247},
note = {},
optannote = {},
errata = {http://www.cl.cam.ac.uk/~pes20/versions-errata.txt},
url = {http://doi.acm.org/10.1145/360204.360225},
doi = {10.1145/360204.360225},
pdf = {http://www.cl.cam.ac.uk/users/pes20/versions-popl.pdf},
abstract = {
In a wide-area distributed system it is often impractical to
synchronise software updates, so one must deal with many
coexisting versions. We study static typing support for modular wide-area programming, modelling separate compilation/linking and execution of programs that interact along
typed channels. Interaction may involve communication of
values of abstract types; we provide the developer with finegrain versioning control of these types to support interoperation of old and new code. The system makes use of a
second-class module system with singleton kinds; we give a
novel operational semantics for separate compilation/linking
and execution and prove soundness.
},
topic = {distributed_types}
}
@techreport{LPSW03-tr,
author = {James Leifer and Gilles Peskine and Peter Sewell and Keith Wansbrough},
title = {Global abstraction-safe marshalling with hash types},
institution = {University of Cambridge Computer Laboratory},
year = {2003},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-569},
optaddress = {},
month = jun,
note = {Also published as INRIA Rocquencourt report RR-4851. 86pp.},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-569.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/hashtypes.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-569.html},
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.},
topic = {distributed_types}
}
@inproceedings{LPSW03,
author = {James Leifer and Gilles Peskine and Peter Sewell and Keith Wansbrough},
title = {Global abstraction-safe marshalling with hash types},
conf = {ICFP 2003},
booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (Uppsala)},
optcrossref = {},
optkey = {},
pages = {87--98},
year = {2003},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = aug,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
url = {http://doi.acm.org/10.1145/944746.944714},
doi = {10.1145/944746.944714},
pdf = {http://www.cl.cam.ac.uk/~pes20/hashtypes.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/hashtypes.ps},
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, 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.},
topic = {distributed_types}
}
@inproceedings{BHSSW03,
author = {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle and Keith Wansbrough},
title = {Dynamic Rebinding for Marshalling and Update, with Destruct-time lambda},
conf = {ICFP 2003},
booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (Uppsala)},
optcrossref = {},
optkey = {},
pages = {99--110},
year = {2003},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = aug,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
url = {http://doi.acm.org/10.1145/944746.944715},
doi = {10.1145/944746.944715},
pdf = {http://www.cl.cam.ac.uk/~pes20/dynbind2-short.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/dynbind2-short.ps},
abstract = {Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too
restrictive: dynamic binding is required in various guises, for example when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically it is provided only by ad-hoc mechanisms that lack clean semantics.
In this paper we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to simply-typed call-by-value lambda-calculus. To do so we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies.
The latter forms the basis for a lambda-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We sketch an extension of lambda-marsh with concurrency and communication, giving examples showing how
wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating
can also be based on the destruct-time strategy, defining a lambda-update calculus with simple primitives to provide type-safe updating of
running code. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding
requirements.
},
topic = {distributed_types_and_update}
}
@techreport{BHSSW04-tr,
author = {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle and Keith Wansbrough},
title = {Dynamic Rebinding for Marshalling and Update, with Destruct-time $\lambda$},
institution = {University of Cambridge Computer Laboratory},
year = {2004},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-568},
optaddress = {},
month = feb,
note = {85pp},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/UCAM-CL-TR-568.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/dynbind2-long-draft.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-568.html},
abstract = {
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically it is provided only by ad-hoc mechanisms that lack clean semantics.
In this paper we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to the simply-typed call-by-value λ-calculus. To do so we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies. The latter forms the basis for a λ-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We sketch an extension of λ-marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a λ-update calculus with simple primitives to provide type-safe updating of running code. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.
},
topic = {distributed_types_and_update}
}
@inproceedings{LNSW04,
author = {James Leifer and Michael Norrish and Peter Sewell and Keith Wansbrough},
title = {Acute and {TCP}: specifying and developing abstractions for global computation},
optcrossref = {},
optkey = {},
conf = {APPSEM II Workshop, 2004},
booktitle = {Proceedings of the APPSEM II Workshop (Tallinn)},
pages = {},
year = {2004},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = apr,
optorganization = {},
optpublisher = {},
note = {2pp},
optannote = {},
topic = {distributed_types}
}
@techreport{SLWAZHV04,
author = {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Mair Allen-Williams and
Zappa Nardelli, Francesco and
Pierre Habouzit and
Viktor Vafeiadis},
title = {Acute: High-level programming language design for distributed
computation. Design rationale and language definition},
institution = {University of Cambridge Computer Laboratory},
year = {2004},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-605},
optaddress = {},
month = oct,
note = {Also published as INRIA RR-5329. 193pp},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/acute/UCAM-CL-TR-605.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/acute/acute2-long.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-605.html},
abstract = {
This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have defined and implemented.
Acute extends an OCaml core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built programs. It is expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs, disentangling the language runtime from communication.
This requires a synthesis of novel and existing features:
(1) type-safe marshalling of values between programs;
(2) dynamic loading and controlled rebinding to local resources;
(3) modules and abstract types with abstraction boundaries that are respected by interaction;
(4) global names, generated either freshly or based on module hashes: at the type level, as runtime names for abstract types; and at the term level, as channel names and other interaction handles;
(5) versions and version constraints, integrated with type identity;
(6) local concurrency and thread thunkification; and
(7) second-order polymorphism with a namecase construct.
We deal with the interplay among these features and the core, and develop a semantic definition that tracks abstraction boundaries, global names, and hashes throughout compilation and execution, but which still admits an efficient implementation strategy.
},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/acute/}
}
@inproceedings{SLWZAHV05,
optnote = {SLWAZHV04-paper},
author = {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Zappa Nardelli, Francesco and
Mair Allen-Williams and
Pierre Habouzit and
Viktor Vafeiadis},
title = {Acute: High-level programming language design for distributed
computation},
optcrossref = {},
optkey = {},
conf = {ICFP 2005},
booktitle = {Proceedings of the 10th ACM SIGPLAN International Conference on
Functional Programming (Tallinn)},
pages = {15--26},
year = {2005},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = sep,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
url = {http://doi.acm.org/10.1145/1086365.1086370},
doi = {10.1145/1086365.1086370},
pdf = {http://www.cl.cam.ac.uk/~pes20/acute/acute2-short.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/acute/acute2-short.ps},
abstract = {
Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there
may be interaction between multiple instances of many distinct pro-grams, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper we discuss programming language support for su
ch systems, focussing on their typing and naming issues.
We describe an experimental language, Acute, which extends an
ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built
programs. The main features are: (1) type-safe marshalling of arbitrary values; (2) type names that are generated (freshly and by
hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system; (3)
expression-level names generated to ensure that name equality tests suffice for type-safety of associated values, e.g.~values carried on
named channels; (4) controlled dynamic rebinding of marshalled values to local resources; and (5) thunkification of threads and mutexes to support computation mobility.
These features are a large part of what is needed for typeful
distributed programming. They are a relatively lightweight extension of
ML, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers
to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language runtime
from communication intricacies. This paper highlights the main design choices in
Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype
implementation, and by example distribution libraries.
},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/acute/}
}
@inproceedings{BSSS06,
author = {John Billings and Peter Sewell and Mark Shinwell and Rok Strni\v sa},
title = {Type-Safe Distributed Programming for {OCaml}},
optcrossref = {},
optkey = {},
conf = {ML 2006},
booktitle = {Proceedings of the 2006 ACM SIGPLAN Workshop on ML},
pages = {20--31},
year = {2006},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = sep,
optorganization = {},
optpublisher = {},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/hashcaml/index.html},
url = {http://doi.acm.org/10.1145/1159876.1159881},
doi = {10.1145/1159876.1159881},
pdf = {http://www.cl.cam.ac.uk/~pes20/hashcaml/paper.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/hashcaml/paper.ps},
abstract = {
Existing ML-like languages guarantee type-safety, ensuring memory safety 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
marshalling within polymorphic functions by type-passing, requiring us to build compositional runtime type names and revisit the
OCaml relaxed value restriction. We show that with typed marshalling one must fall back to the SML97 value restriction. (3) We
show how the above can be implemented with reasonable performance as an unintrusive modification to the existing OCaml language, implementation, and standard libraries. An alpha release of HashCaml, capable of bootstrapping itself, is available, along with
an example type-safe distributed communication library written in the language.
},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/hashcaml/}
}
@article{SLWZAHV-jfp,
author = {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Zappa Nardelli, Francesco and
Mair Allen-Williams and
Pierre Habouzit and
Viktor Vafeiadis},
title = {Acute: High-level programming language design for distributed
computation},
optjournal = {J. Functional Programming},
journal = {Journal of Functional Programming},
year = {2007},
optkey = {},
volume = {17},
number = {4--5},
pages = {547--612},
month = jul,
note = {Invited submission for an ICFP 2005 special issue},
optannote = {},
project = {http://www.cl.cam.ac.uk/~pes20/acute/index.html},
pdf = {http://www.cl.cam.ac.uk/~pes20/acute/paper3.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/acute/paper3.ps},
url = {https://doi.org/10.1017/S0956796807006442},
doi = {10.1017/S0956796807006442},
abstract = {
Existing languages provide good support for typeful programming of stand-alone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper, we discuss programming-language support for such systems, focussing on their typing and naming issues. We describe an experimental language, Acute, which extends an ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately built programs. The main features are (1) type-safe marshalling of arbitrary values; (2) type names that are generated (freshly and by hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system; (3) expression-level names generated to ensure that name equality tests suffice for type safety of associated values, for example, values carried on named channels; (4) controlled dynamic rebinding of marshalled values to local resources; and (5) thunkification of threads and mutexes to support computation mobility. These features are a large part of what is needed for typeful distributed programming. They are a relatively lightweight extension of ML, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language run-time from communication intricacies. This paper highlights the main design choices in Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype implementation, and by example distribution libraries.},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/acute/}
}
@article{BHSSW-jfp,
author = {Peter Sewell and Gareth Stoyle and Michael Hicks and Gavin Bierman and Keith Wansbrough},
title = {Dynamic Rebinding for Marshalling and Update, via Redex-time and Destruct-time Reduction},
journal = {Journal of Functional Programming},
year = {2008},
optkey = {},
volume = {18},
number = {4},
pages = {437--502},
optmonth = {},
optnote = {66pp.},
optannote = {},
doi = {https://doi.org/10.1017/S0956796807006600},
pdf = {http://www.cl.cam.ac.uk/~pes20/jfp2008.pdf},
abstract = {
Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example, when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically, it is provided only by ad hoc mechanisms that lack clean semantics. In this paper, we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to the simply typed call-by-value lambda calculus. To do so, we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies. The latter forms the basis for a lambda-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically typed. We sketch an extension of lambda-marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a lambda-update calculus with simple primitives to provide type-safe updating of running code. We show how the ideas of this simple calculus extend to more real-world, module-level dynamic updating in the style of Erlang. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.},
topic = {distributed_types_and_update}
}
@misc{acute-release-0-50-1,
optnote = {acute-release},
author = {Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Mair Allen-Williams and
Zappa Nardelli, Francesco and
Pierre Habouzit and
Viktor Vafeiadis},
title = {Acute release},
optinstitution = {University of Cambridge Computer Laboratory},
year = {2005},
optkey = {},
opttype = {},
optnumber = {},
optaddress = {},
month = jan,
optnote = {Available from \url{http://www.cl.cam.ac.uk/users/pes20/acute/distro/acute-0.50-1-src.tar.gz}},
optannote = {},
url = {http://www.cl.cam.ac.uk/users/pes20/acute/distro/acute-0.50-1-src.tar.gz},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/acute/}
}
@misc{hashcaml-release,
optkey = {},
author = {John Billings and Peter Sewell and Mark Shinwell and Rok Strni\v sa},
title = {{HashCaml} release, version 3.09.1-alpha-795},
opthowpublished = {},
month = apr,
year = {2006},
optnote = {\url{http://www.cl.cam.ac.uk/~pes20/hashcaml/index.html}},
url = {http://www.cl.cam.ac.uk/~pes20/hashcaml/index.html},
optannote = {},
topic = {distributed_types},
project = {http://www.cl.cam.ac.uk/~pes20/hashcaml/}
}