topic.dynamic_update.bib

@comment{{This file has been generated by bib2bib 1.96}}
@comment{{Command line: /usr/bin/bib2bib -c 'topic:"dynamic_update" or topic:"distributed_types_and_update"' -ob topic.dynamic_update.bib sewellbib2.bib}}
@inproceedings{BHSS03,
  author = {Gavin Bierman and Michael Hicks and Peter Sewell and Gareth Stoyle},
  title = {Formalizing Dynamic Software Updating},
  conf = {USE 2003},
  booktitle = {Proceedings of  the Second International Workshop on Unanticipated Software
                                            Evolution (Warsaw), in conjunction with ETAPS},
  optcrossref = {},
  optkey = {},
  optpages = {},
  year = {2003},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = apr,
  optorganization = {},
  optpublisher = {},
  note = {17pp},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/formalUpdate.pdf},
  ps = {http://www.cl.cam.ac.uk/users/pes20/formalUpdate.ps},
  abstract = {Dynamic software updating (DSU) enables running programs to be
updated with new code and data without interrupting their execution. A
number of DSU systems have been designed, but there is still little rigorous und
erstanding of how to use DSU technology so that updates are
safe. As a first step in this direction, we introduce a small update calculus
with a precise mathematical semantics. The calculus is formulated as an
extension of a typed lambda calculus, and supports updating technology
similar to that of the programming language Erlang [2]. Our goal is to
provide a simple yet expressive foundation for reasoning about dynamically updat
eable software. In this paper, we present the details of the
calculus, give some examples of its expressive power, and discuss how it
might be used or extended to guarantee safety properties.},
  topic = {dynamic_update}
}
@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{SHBSN05,
  author = {Gareth Stoyle and
Michael Hicks and
Gavin Bierman and
Peter Sewell and
Iulian Neamtiu},
  title = {\textit{Mutatis Mutandis}: Safe and Predictable Dynamic Software Updating},
  optcrossref = {},
  optkey = {},
  conf = {POPL 2005},
  booktitle = {Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Long Beach)},
  pages = {183--194},
  year = {2005},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = jan,
  optorganization = {},
  optpublisher = {},
  optnote = {},
  optannote = {},
  url = {http://doi.acm.org/10.1145/1255450.1255455},
  doi = {10.1145/1255450.1255455},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/update-popl-2005.pdf},
  abstract = {
Dynamic software updates can be used to fix bugs or add features 
  to a running program without downtime. Essential for some applications and convenient for others, low-level dynamic updating has 
  been used for many years. Perhaps surprisingly, there is little high-level understanding or language support to help programmers write 
  dynamic updates effectively. 

  To bridge this gap, we present Proteus, a core calculus for dynamic software updating in C-like languages that is flexible, safe, 
    and predictable. Proteus supports dynamic updates to functions 
    (even active ones), to named types and to data, allowing on-line 
    evolution to match source-code evolution as we have observed it 
    in practice. We ensure updates are type-safe by checking for a 
    property we call ``con-freeness'' for updated types t at the point 
        of update. This means that non-updated code will not use t concretely beyond that point (concrete usages are via explicit coercions) and thus t's representation can safely change. We show how 
          con-freeness can be enforced dynamically for a particular program 
          state. We additionally define a novel and efficient static updateability analysis to establish con-freeness statically, and can thus automatically infer program points at which all future (well-formed) 
              updates will be type-safe. We have implemented our analysis for C 
              and tested it on several well-known programs. 
},
  topic = {dynamic_update}
}
@article{SHBSN-toplas,
  optnote = {1255455},
  author = {Gareth Stoyle and Michael Hicks and Gavin Bierman and Peter Sewell and Iulian Neamtiu},
  title = {Mutatis Mutandis: Safe and predictable dynamic software updating},
  journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
  optjournal = {ACM TOPLAS},
  volume = {29},
  number = {4},
  year = {2007},
  month = aug,
  issn = {0164-0925},
  pages = {70pp},
  optnote = {70pp},
  doi = {http://doi.acm.org/10.1145/1255450.1255455},
  publisher = {ACM Press},
  address = {New York, NY, USA},
  pdf = {http://portal.acm.org/ft_gateway.cfm?id=1255455&type=pdf&coll=portal&dl=ACM&CFID=5852982&CFTOKEN=74490170},
  abstract = {This article presents Proteus, a core calculus that models dynamic software updating, a service for fixing bugs and adding features to a running program. Proteus permits a program's type structure to change dynamically but guarantees the updated program remains type-correct by ensuring a property we call con-freeness. We show how con-freeness can be enforced dynamically, and how it can be approximated via a novel static analysis. This analysis can be used to assess the implications of a program's structure on future updates in order to make update success more predictable. We have implemented Proteus for C, and briefly discuss our implementation which we have tested on several well-known programs.},
  topic = {dynamic_update}
}
@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}
}