{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:56:11Z","timestamp":1776891371905,"version":"3.51.2"},"reference-count":77,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"4","license":[{"start":{"date-parts":[[2007,10,17]],"date-time":"2007-10-17T00:00:00Z","timestamp":1192579200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2008,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    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 \u03bb 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\n                    <jats:italic>redex<\/jats:italic>\n                    -\n                    <jats:italic>time<\/jats:italic>\n                    and\n                    <jats:italic>destruct<\/jats:italic>\n                    -\n                    <jats:italic>time<\/jats:italic>\n                    strategies. The latter forms the basis for a \u03bb\n                    <jats:sub>marsh<\/jats:sub>\n                    calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically typed. We sketch an extension of \u03bb\n                    <jats:sub>marsh<\/jats:sub>\n                    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 \u03bb\n                    <jats:sub>update<\/jats:sub>\n                    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.\n                  <\/jats:p>","DOI":"10.1017\/s0956796807006600","type":"journal-article","created":{"date-parts":[[2007,10,17]],"date-time":"2007-10-17T08:51:05Z","timestamp":1192611065000},"page":"437-502","source":"Crossref","is-referenced-by-count":4,"title":["Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction"],"prefix":"10.46298","volume":"18","author":[{"given":"PETER","family":"SEWELL","sequence":"first","affiliation":[]},{"given":"GARETH","family":"STOYLE","sequence":"additional","affiliation":[]},{"given":"MICHAEL","family":"HICKS","sequence":"additional","affiliation":[]},{"given":"GAVIN","family":"BIERMAN","sequence":"additional","affiliation":[]},{"given":"KEITH","family":"WANSBROUGH","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2007,10,17]]},"reference":[{"key":"S0956796807006600_manual_ref-55","doi-asserted-by":"publisher","DOI":"10.1145\/1133255.1133991"},{"key":"S0956796807006600_manual_ref-52","unstructured":"MIT. (n.d.) MIT Scheme. Available at: http:\/\/www.swiss.ai.mit.edu\/projects\/scheme\/. Accessed Sept 2007."},{"key":"S0956796807006600_manual_ref-59","unstructured":"Potter, S. & Nieh, J. (2005 December) Reducing downtime due to system maintenance and upgrades. In Proceedings of LISA: The 19th Conference on Systems Administration (San Diego). 47\u201362."},{"key":"S0956796807006600_manual_ref-67","first-page":"1","volume-title":"Internet Programming Languages, LNCS 1686","author":"Sewell","year":"1999"},{"key":"S0956796807006600_manual_ref-30","doi-asserted-by":"publisher","DOI":"10.1145\/62678.62684"},{"key":"S0956796807006600_manual_ref-7","unstructured":"Armstrong, J. , Virding, R. , Wikstrom, C. & Williams, M. (1996) Concurrent Programming in Erlang, 2nd ed. Englewood Cliffs, NJ, USA. Prentice Hall."},{"key":"S0956796807006600_manual_ref-38","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00174-2"},{"key":"S0956796807006600_manual_ref-42","first-page":"147","volume-title":"Proceedings of TIC: the 3rd International Workshop on Types in Compilation (Montreal), Revised Selected Papers, LNCS 2071","author":"Hicks","year":"2000"},{"key":"S0956796807006600_manual_ref-25","first-page":"85","volume-title":"Proceedings of TIC: The 3rd International Workshop on Types in Compilation (Montreal), Revised Selected Papers, LNCS 2071","author":"Duggan","year":"2000"},{"key":"S0956796807006600_manual_ref-49","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158706"},{"key":"S0956796807006600_manual_ref-4","unstructured":"Altekar, G. , Bagrak, I. , Burstein, P. & Schultz, A. (2005 August) OPUS: Online patches and updates for security. In Proceedings of 14th USENIX Security Symposium. USENIX, Berkeley, CA, USA. pp. 287\u2013302."},{"key":"S0956796807006600_manual_ref-57","unstructured":"Pai, V. S. , Druschel, P. & Zwaenepoel, W. (1999 June) Flash: An efficient and portable webserver. In Proceedings of the USENIX Annual Technical Conference. pp. 106\u2013119."},{"key":"S0956796807006600_manual_ref-61","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292551"},{"key":"S0956796807006600_manual_ref-12","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944715"},{"key":"S0956796807006600_manual_ref-16","unstructured":"Boa. (n.d.) Boa webserver. Available at: http:\/\/www.boa.org. Accessed Sept 2007."},{"key":"S0956796807006600_manual_ref-56","first-page":"315","volume-title":"Distributed Systems","author":"Needham","year":"1993"},{"key":"S0956796807006600_manual_ref-21","first-page":"1","article-title":"A distributed pi-calculus with local areas of communication","volume":"41","author":"Chothia","year":"2000","journal-title":"Proceedings of HLCL: The 4th International Workshop on High-Level Concurrent Languages (Montreal), published as Electr. Notes Theor. Comput. Sci."},{"key":"S0956796807006600_manual_ref-20","doi-asserted-by":"publisher","DOI":"10.1145\/1134760.1134767"},{"key":"S0956796807006600_manual_ref-40","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378798"},{"key":"S0956796807006600_manual_ref-63","first-page":"563","volume-title":"IFIP Conference Proceedings","author":"Schmitt","year":"2002"},{"key":"S0956796807006600_manual_ref-66","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2000.856943"},{"key":"S0956796807006600_manual_ref-75","doi-asserted-by":"publisher","DOI":"10.1145\/363911.363923"},{"key":"S0956796807006600_manual_ref-53","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010087314987"},{"key":"S0956796807006600_manual_ref-2","unstructured":"Ajmani, S. (2004) A review of software upgrade techniques for distributed systems. Available at: http:\/\/pmg.csail.mit.edu\/~ajmani\/papers\/review.pdf. Accessed Sept 2007."},{"key":"S0956796807006600_manual_ref-5","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00104-X"},{"key":"S0956796807006600_manual_ref-14","unstructured":"Billings, J. (2005) A Bytecode Compiler for Acute. Computer Science Tripos Part II Dissertation, University of Cambridge."},{"key":"S0956796807006600_manual_ref-68","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086370"},{"key":"S0956796807006600_manual_ref-71","unstructured":"Squeak. (n.d.) Squeak Smalltalk-80 Programming system. Available at: http:\/\/www.squeak.org"},{"key":"S0956796807006600_manual_ref-64","unstructured":"Serra, A. Navarro, N. & Cortes, T. (2000) DITools: Application-level support for dynamic extension and flexible composition. In Proc. USENIX Annual Technical Conference. pp. 225\u2013238."},{"key":"S0956796807006600_manual_ref-43","unstructured":"Hirschowitz, T. (2003) Modules mixins, modules et r\u00e9cursion \u00e9tendue en appel par valeur, Th\u00e8se de doctorat. Universit\u00e9 Paris 7."},{"key":"S0956796807006600_manual_ref-51","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325708"},{"key":"S0956796807006600_manual_ref-15","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159881"},{"key":"S0956796807006600_manual_ref-34","unstructured":"Gilmore, S. , Kirli, D. & Walton, C. (1997) Dynamic ML Without Dynamic Types. Tech. Rept. ECS-LFCS-97-378. Dept. of Computer Science, The University of Edinburgh."},{"key":"S0956796807006600_manual_ref-31","first-page":"406","volume-title":"Proceedings of CONCUR '96: The 7th International Conference on Concurrency Theory (Pisa), LNCS 1119","author":"Fournet","year":"1996"},{"key":"S0956796807006600_manual_ref-77","doi-asserted-by":"publisher","DOI":"10.1145\/502059.502057"},{"key":"S0956796807006600_manual_ref-9","unstructured":"Baumann, A. , Appavoo, J. , Silva, D. Da , Krieger, O. & Wisniewski, R. (2004 October). Improving operating system availability with dynamic update. In Proceedings of the Workshop on Operating System and Architectural Support for the on demand IT InfraStructure (OASIS) (Boston). pp. 21\u201327."},{"key":"S0956796807006600_manual_ref-23","unstructured":"dlopen. (n.d.) POSIX dlopen specification. Available at: http:\/\/www.opengroup.org\/onlinepubs\/007904975\/functions\/dlopen.html Accessed Sept 2007."},{"key":"S0956796807006600_manual_ref-35","unstructured":"Goldberg, A. & Robson, D. (1989) Smalltalk 80\u2013-The Language and Its Implementation. Reading MA: Addison-Wesley."},{"key":"S0956796807006600_manual_ref-27","unstructured":"Fabry, R. S. (1976) How to design a system in which modules can be changed on the fly. In Proceedings of the International Conference on Software Engineering (ICSE). pp. 470\u2013476."},{"key":"S0956796807006600_manual_ref-11","doi-asserted-by":"publisher","DOI":"10.1145\/944746.944715"},{"key":"S0956796807006600_manual_ref-26","doi-asserted-by":"crossref","unstructured":"Duggan, D. (2001) Type-based hot swapping of running modules. In Proc. 5th ICFP: The ACM SIGPLAN International Conference on Functional Programming (Firenze). pp. 62\u201373.","DOI":"10.1145\/507635.507645"},{"key":"S0956796807006600_manual_ref-37","unstructured":"Gupta, D. (1994 November) On-line Software Version Change, Ph.D. thesis. Kanpur, India: Department of Computer Science and Engineering, Indian Institute of Technology."},{"key":"S0956796807006600_manual_ref-44","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888267"},{"key":"S0956796807006600_manual_ref-62","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(96)00032-3"},{"key":"S0956796807006600_manual_ref-70","unstructured":"Soules, C. , Appavoo, J. , Hui, K. , Silva, D. Da , Ganger, G. , Krieger, O. , Stumm, M. , Wisniewski, R. , Auslander, M. , Ostrowski, M. , Rosenburg, B. & Xenidis, J. (2003 June) System support for online reconfiguration. In Proceedings of the USENIX Annual Technical Conference (San Antonio). pp. 141\u2013154."},{"key":"S0956796807006600_manual_ref-60","doi-asserted-by":"publisher","DOI":"10.1145\/181889.181891"},{"key":"S0956796807006600_manual_ref-54","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58402-1_14"},{"key":"S0956796807006600_manual_ref-10","doi-asserted-by":"crossref","unstructured":"Baumann, A. , Appavoo, J. , Silva, D. Da , Kerr, J. , Krieger, O. & Wisniewski, R. W. (2005) Providing dynamic update in an operating system. In Proceedings of the USENIX Annual Technical Conference (Anaheim, CA). USENIX. pp. 279\u2013291.","DOI":"10.1145\/1095810.1118622"},{"key":"S0956796807006600_manual_ref-36","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224173"},{"key":"S0956796807006600_manual_ref-29","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"S0956796807006600_manual_ref-45","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177578"},{"key":"S0956796807006600_manual_ref-58","volume-title":"Principled Dynamic Code Improvement.","author":"Peterson","year":"1997"},{"key":"S0956796807006600_manual_ref-3","first-page":"452","volume-title":"Proc. ECOOP, the 20th European Conference on Object-Oriented Programming (Nantes, France), LNCS 4067","author":"Ajmani","year":"2006"},{"key":"S0956796807006600_manual_ref-32","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(91)90096-O"},{"key":"S0956796807006600_manual_ref-19","unstructured":"Carlsson, Richard , Gustavsson, Bj\u00f6rn , Johannson, Erik , Lindgren, Thomas , Nystr\u00f6m, Svel-Olof , Pettersson, Mikael , & Virding, Robert . 2004 (Nov.). Core Erlang 1.0.3 language specification. http:\/\/www.it.uu.se\/research\/group\/hipe\/cerl\/. Accessed Sept 2007."},{"key":"S0956796807006600_manual_ref-41","volume-title":"A Calculus for Dynamic Loading.","author":"Hicks","year":"2000"},{"key":"S0956796807006600_manual_ref-22","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00150-3"},{"key":"S0956796807006600_manual_ref-28","first-page":"193","volume-title":"Formal Description of Programming Concepts III","author":"Felleisen","year":"1987"},{"key":"S0956796807006600_manual_ref-6","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"S0956796807006600_manual_ref-1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96712"},{"key":"S0956796807006600_manual_ref-50","volume-title":"The Objective Caml System Release 3.04 Documentation","author":"Leroy","year":"2001"},{"key":"S0956796807006600_manual_ref-76","unstructured":"Walton, C. (2001) Abstract Machines for Dynamic Computation, Ph.D. thesis. University of Edinburgh. ECS-LFCS-01-425."},{"key":"S0956796807006600_manual_ref-24","unstructured":"Drossopoulou, S. & Eisenbach, S. (2002 June) Manifestations of dynamic linking. In Proceedings of the 1st Workshop on Unanticipated Software Evolution (USE 2002). Available at: http:\/\/slurp.doc.ic.ac.uk\/pubs\/manifestations-use02.pdf. Accessed Sept 2007."},{"key":"S0956796807006600_manual_ref-46","unstructured":"Java. (n.d.) Java platform debugger architecture. (This supports class replacement). Available at: http:\/\/java.sun.com\/j2se\/1.4.2\/docs\/guide\/jpda\/. Accessed Sept 2007."},{"key":"S0956796807006600_manual_ref-8","unstructured":"Barklund, J. & Virding, R. (1999 February) Erlang 4.7.3 reference manual DRAFT (0.7). Available at: http:\/\/www.erlang.org\/download\/erl_spec47.ps.gz. Accessed Sept 2007."},{"key":"S0956796807006600_manual_ref-73","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040321"},{"key":"S0956796807006600_manual_ref-39","first-page":"198","volume-title":"Proc. COORDINATION (Limassol, Cyprus), LNCS 1906","author":"Hashimoto","year":"2000"},{"key":"S0956796807006600_manual_ref-13","unstructured":"Bierman, G. , Hicks, M. , Sewell, P. & Stoyle, G. (2003c April). Formalizing dynamic software updating. In Proceedings of USE 2003: The Second International Workshop on Unanticipated Software Evolution (Warsaw)."},{"key":"S0956796807006600_manual_ref-48","unstructured":"Lee, I. (1983 April) DYMOS: A dynamic modification system. Ph.D. thesis. Madison: Department of Computer Science, University of Wisconsin."},{"key":"S0956796807006600_manual_ref-69","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006442"},{"key":"S0956796807006600_manual_ref-74","unstructured":"Vivas Frontana, J. L. , (2001 March) Dynamic Binding of Names in Calculi for Mobile Processes, Ph.D. thesis. Stockholm: KTH."},{"key":"S0956796807006600_manual_ref-72","unstructured":"Stoyle, G. (2006) A Theory of Dynamic Software Updates, Ph.D. thesis. University of Cambridge."},{"key":"S0956796807006600_manual_ref-47","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159808"},{"key":"S0956796807006600_manual_ref-33","first-page":"14","volume-title":"Proceedings of the Fuji International Workshop on Functional and Logic Programming","author":"Garrigue","year":"1995"},{"key":"S0956796807006600_manual_ref-65","first-page":"391","volume-title":"Proceedings of CONCUR 97: Concurrency Theory (Warsaw). LNCS 1243","author":"Sewell","year":"1997"},{"key":"S0956796807006600_manual_ref-18","first-page":"140","volume-title":"Proc. FoSSaCS: 1st International Conference on Foundations of Software Science and Computation Structure, as part of ETAPS (Lisbon), LNCS 1378","author":"Cardelli","year":"1998"},{"key":"S0956796807006600_manual_ref-17","doi-asserted-by":"publisher","DOI":"10.1145\/949343.949341"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796807006600","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:10Z","timestamp":1776889150000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796807006600\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,17]]},"references-count":77,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["S0956796807006600"],"URL":"https:\/\/doi.org\/10.1017\/s0956796807006600","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10,17]]}}}