M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin, Dynamic typing in a statically typed language, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.13, issue.2, 1991.

F. Acherman, Forms, agents and channels, 2002.

J. Aldrich, C. Chambers, and D. Notkin, Architectural Reasoning in ArchJava, Proceedings 16th European Conference on Object-Oriented Programming, 2002.
DOI : 10.1007/3-540-47993-7_15

J. Aldrich, V. Sazawal, C. Chambers, and D. Notkin, Language Support for Connector Abstractions, Proceedings 17th European Conference on Object-Oriented Programming, 2003.
DOI : 10.1007/978-3-540-45070-2_5

M. Alia, S. Chassande-barrioz, P. Déchamboux, C. Hamon, and A. Lefebvre, A Middleware Framework for the Persistence and Querying of Java Objects, Proceedings ECOOP 2004, number 3086 in Lecture Notes in Computer Science, 2004.
DOI : 10.1007/978-3-540-24851-4_14

R. Allen, R. Douence, and D. Garlan, Specifying and analyzing dynamic software architectures, Proceedings of the 1998 Conference on Fundamental Approaches to Software Engineering (FASE'98), 1998.
DOI : 10.1007/BFb0053581
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5206

R. Allen, D. Garlan, and R. Douence, Specifying Dynamism in Software Architectures, Proceedings of the Workshop on Foundations of Component-Based Software Engineering, 1997.

D. Ancona and E. Zucca, A calculus of module systems, Journal of Functional Programming, vol.12, issue.02, 2002.
DOI : 10.1017/S0956796801004257

J. Armstrong, Making reliable distributed systems in the presence of software errors, KTH, 2003.

R. Armstrong, D. Gannon, A. Geist, K. Keahey, S. R. Kohn et al., Toward a common component architecture for high-performance scientific computing, Proceedings. The Eighth International Symposium on High Performance Distributed Computing (Cat. No.99TH8469), 1999.
DOI : 10.1109/HPDC.1999.805289

K. Arnold, J. Gosling, and D. Holmes, The Java Programming Language, 2005.

R. Balter, L. Bellissard, F. Boyer, M. Riveill, and J. Y. Vion-dury, Architecturing and configuring distributed applications with olan The Lake District, Proceedings IFIP Int. Conf. on Distributed Systems Platforms and Open Distributed Processing (Middleware'98), 1998.

J. P. Banâtre, P. Fradet, and Y. Radenac, Higher-Order Chemical Programming Style, Unconventional Programming Paradigms, International Workshop UPP 2004, Revised Selected and Invited Papers, 2005.
DOI : 10.1007/11527800_7

J. P. Banâtre, P. Fradet, and Y. Radenac, A Generalized Higher-Order Chemical Computation Model, Electronic Notes in Theoretical Computer Science, vol.135, issue.3, 2006.
DOI : 10.1016/j.entcs.2005.09.016

M. Berger, Basic theory of reduction congruence for two timed asynchronous pi-calculi, CONCUR 2004 -Concurrency Theory, 15th International Conference, 2004.

L. Bettini, V. Bono, R. De-nicola, G. Ferrari, D. Gorla et al., The Klaim Project: Theory and Practice, Global Computing: Programming Environments, Languages, Security and Analysis of Systems, number 2874 in Lecture Notes in Computer Science, 2003.
DOI : 10.1007/978-3-540-40042-4_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.9766

L. Bettini, V. Bono, and B. Venneri, O???Klaim: A??Coordination Language with Mobile Mixins, Proceedings of Coordination, 2004.
DOI : 10.1007/3-540-48320-9_38

P. Bidinger, M. Leclercq, V. Quéma, A. Schmitt, and J. B. Stefani, Dream Types -A Domain Specific Type System for Component-Based Message-Oriented Middleware, 4th Workshop on Specification and Verification of Component-Based Systems (SAVCBS'05), in association with ESEC/FSE'05, 2005.

P. Bidinger, A. Schmitt, and J. Stefani, An Abstract Machine for the Kell Calculus, Formal Methods for Open Object-Based Distributed Systems (FMOODS), 7th IFIP WG 6.1 International Conference, 2005.
DOI : 10.1007/3-540-47959-7_3

A. D. Birrell, G. Nelson, S. Owicki, and E. Wobber, Network objects, Proceedings 14th Symp. on Operating Systems Principles (SOSP), 1993.

T. Bloom, Dynamic Module Replacement in a Distributed Programming System, 1983.

S. Bouchenak, F. Boyer, S. Krakowiak, D. Hagimont, A. Mos et al., Architecture-based autonomous repair management: An application to j2ee clusters, 24th IEEE Symposium on Reliable Distributed Systems (SRDS 2005, 2005.
DOI : 10.1109/reldis.2005.8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.109.6765

G. Boudol, ULM: A Core Programming Model for Global Computing, European Symposium on Programming (ESOP), Lecture Notes in Computer Science, 2004.
DOI : 10.1007/978-3-540-24725-8_17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.58.9093

J. Bradbury, J. Cordy, J. Dingel, and M. Wermelinger, A survey of self-management in dynamic software architecture specifications, Proceedings of the 1st ACM SIGSOFT workshop on Self-managed systems , WOSS '04, 2004.
DOI : 10.1145/1075405.1075411

E. Bruneton, T. Coupaye, M. Leclercq, V. Quema, and J. B. Stefani, The Fractal Component Model and its Support in Java. Software -Practice and Experience, pp.11-12, 2006.

E. Bruneton, T. Coupaye, and J. Stefani, The Fractal Component Model, The ObjectWeb Consortium, 2004.

R. Bruni, H. C. Melgratti, and U. Montanari, Theoretical foundations for compensations in flow composition languages, POPL. ACM, 2005.

L. Cardelli, Program fragments, linking, and modularization, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, 1997.
DOI : 10.1145/263699.263735
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.8472

G. Castagna, J. Vitek, and F. Z. Nardelli, The seal calculus. Information and Computation, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00152521

H. Cejtin, S. Jagannathan, and R. Kelsey, Higher-order distributed objects, ACM Transactions on Programming Languages and Systems, vol.17, issue.5, 1995.
DOI : 10.1145/213978.213986
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.9759

K. Chandy and J. Misra, Parallel Program Design -A Foundation, 1988.

S. W. Cheng, A. C. Huang, D. Garlan, B. R. Schmerl, and P. Steenkiste, Rainbow: Architecture-based selfadaptation with reusable infrastructure, 1st International Conference on Autonomic Computing, 2004.

D. Clarke, J. Noble, and J. Potter, Simple Ownership Types for Object Containment, Proceedings ECOOP, 2001.
DOI : 10.1007/3-540-45337-7_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.9675

D. Clarke and T. Wrigstad, External Uniqueness Is Unique Enough, Proceedings 17th European Conference on Object-Oriented Programming, 2003.
DOI : 10.1007/978-3-540-45070-2_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.109.1645

M. Clarke, G. Blair, G. Coulson, and N. Parlavantzas, An Efficient Component Model for the Construction of Adaptive Middleware, Proceedings of the IFIP/ACM International Conference on Distributed Systems Platforms (Middleware'01), pp.160-178, 2001.
DOI : 10.1007/3-540-45518-3_9

R. Collet and P. Van-roy, Failure Handling in a Network-Transparent Distributed Programming Language, Recent Advances in Exception Handling Techniques, 2006.
DOI : 10.1007/11818502_7

G. Coulson, G. Blair, P. Grace, A. Joolia, K. Lee et al., OpenCOM v2: A Component Model for Building Systsms Software, Proceedings of IASTED Software Engineering and Applications (SEA '04), 2004.

V. Danos and J. Krivine, Reversible Communicating Systems, In CONCUR Lecture Notes in Computer Science, vol.6, issue.4, 2004.
DOI : 10.1007/BFb0012800
URL : https://hal.archives-ouvertes.fr/hal-00784051

V. Danos and J. Krivine, Transactions in RCCS, CONCUR 2005 -Concurrency Theory, 16th International Conference, 2005.
DOI : 10.1007/11539452_31
URL : https://hal.archives-ouvertes.fr/hal-00164585

P. C. David and T. Ledoux, Towards a Framework for Self-adaptive Component-Based Applications, DAIS, volume 2893 of LNCS, 2003.
DOI : 10.1007/3-540-40002-8_12
URL : https://hal.archives-ouvertes.fr/hal-00457083

B. Dumant, F. Dang-tran, F. Horn, and J. B. Stefani, Jonathan: an open distributed platform in Java, Distributed Systems Engineering Journal, vol.6, 1999.
DOI : 10.1007/978-1-4471-1283-9_11

M. Fahndrich, M. Aiken, C. Hawblitzel, O. Hodson, G. Hunt et al., Language Support for Fast and Reliable Message-based Communication in Singularity OS, 1st EuroSys Conference, 2006.

J. Fassino, J. Stefani, J. Lawall, and G. Muller, THINK: A Software Framework for Component-based Operating System Kernels, USENIX Annual Technical Conference, 2002.

C. Fournet, F. Le-fessant, L. Maranget, and A. Schmitt, JoCaml: A Language for Concurrent Distributed and Mobile Programming, Summer Schol Adv. Functional Programming, 2003.
DOI : 10.1007/978-3-540-44833-4_5

N. Francez and I. Forman, Interacting Processes : A multiparty approach to coordinated distributed programming, 1996.

D. Garlan, R. Monroe, and D. Wile, Acme, CASCON First Decade High Impact Papers on, CASCON '10, 2000.
DOI : 10.1145/1925805.1925814

D. Gelernter, Generative communication in Linda, ACM Transactions on Programming Languages and Systems, vol.7, issue.1, 1985.
DOI : 10.1145/2363.2433

D. Gelernter and N. Carriero, Coordination languages and their significance, Communications of the ACM, vol.35, issue.2, 1992.
DOI : 10.1145/129630.376083

J. C. Godskesen and T. T. Hildebrandt, Extending Howe???s Method to Early Bisimulations for Typed Mobile Embedded Resources with Local Names, Foundations of Software Technology and Theoretical Computer Science, 25th International Conference (FSTTCS), 2005.
DOI : 10.1007/11590156_11

J. Gosling, B. Joy, G. Steele, and G. Bracha, The Java Language Specification, 2005.

D. Gupta, P. Jalote, and G. Barua, A formal framework for on-line software version change, IEEE Transactions on Software Engineering, vol.22, issue.2, 1996.
DOI : 10.1109/32.485222
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.2023

S. Haridi and N. Franzen, Tutorial of Oz Available at the URL, 2004.

S. Haridi, P. Van-roy, P. Brand, M. Mehl, R. Scheidhauer et al., Efficient logic variables for distributed computing, ACM Transactions on Programming Languages and Systems, vol.21, issue.3, 1999.
DOI : 10.1145/319301.319347
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.132.2730

M. Hennessy, J. Rathke, and N. Yoshida, SafeDpi: a language for controlling mobile code, Acta Informatica, vol.42, pp.4-5, 2005.

J. N. Herder, H. Bos, B. Gras, P. Homburg, and A. S. Tanenbaum, Reorganizing UNIX for Reliability, Advances in Computer Systems Architecture, 11th Asia-Pacific Conference, 2006.
DOI : 10.1007/11859802_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.81.318

M. W. Hicks and S. Nettles, Dynamic software updating, ACM Trans. Program. Lang. Syst, vol.27, issue.6, 2005.
DOI : 10.1145/381694.378798
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.135.2437

D. Hirschkoff, T. Hirschowitz, D. Pous, A. Schmitt, and J. B. Stefani, Component-Oriented Programming with Sharing: Containment is Not Ownership, Generative Programming and Component Engineering, 4th International Conference, 2005.
DOI : 10.1007/11561347_26
URL : https://hal.archives-ouvertes.fr/hal-00310126

. Ibm and . Bea, Service Component Architecture - Assem- bly Model Specification Specification available at URL: http, 2005.

Y. Jaradin, F. Spiessens, and P. Van-roy, Capability Confinement by Membranes, Dep. of Comp. Science and Eng, 2005.

S. Katz, A superimposition control construct for distributed systems, ACM Transactions on Programming Languages and Systems, vol.15, issue.2, 1993.
DOI : 10.1145/169701.169682

D. Kozen, Results on the Propositional ??-Calculus, DAIMI Report Series, vol.11, issue.146, 1983.
DOI : 10.7146/dpb.v11i146.7420
URL : http://dx.doi.org/10.1016/0304-3975(82)90125-6

O. Layaida and D. Hagimont, Designing Self-adaptive Multimedia Applications Through Hierarchical Reconfiguration, DAIS, 2005.
DOI : 10.1007/3-540-44763-6_13
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.2973

M. Leclercq, V. Quema, and J. B. Stefani, DREAM, Proceedings of the 3rd workshop on Adaptive and reflective middleware -, 2005.
DOI : 10.1145/1028613.1028625
URL : https://hal.archives-ouvertes.fr/hal-00881539

E. Lee, The Problem with Threads, Computer, vol.39, issue.5, 2006.
DOI : 10.1109/MC.2006.180

Y. Liu and S. Smith, A Formal Framework for Component Deployment, 20th ACM Int. Conf. Object- Oriented Programming, Systems, Languages and Applications (OOPSLA), 2006.

Y. D. Liu and S. Smith, Interaction-Based Programming with Classages, Proceedings OOPSLA, 2005.
DOI : 10.1145/1094811.1094827

Y. D. Liu and S. F. Smith, Modules with Interfaces for Dynamic Linking and Communication, Proceedings European Conf. on Object-Oriented Programming, 2004.
DOI : 10.1007/978-3-540-24851-4_19

D. Luckham and J. Vera, An event-based architecture definition language, IEEE Transactions on Software Engineering, vol.21, issue.9, 1995.
DOI : 10.1109/32.464548

M. Lumpe, F. Achermann, and O. Nierstrasz, A Formal Language for Composition, chapter 4, 2000.

J. Magee, N. Dulay, S. Eisenbach, and J. Kramer, Specifying distributed software architectures, Proceedings 5th European Software Engineering Conference, 1995.
DOI : 10.1007/3-540-60406-5_12
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.7933

J. Magee and J. Kramer, Dynamic structure in software architectures, Proceedings 4th ACM Symp. on Foundations of Soft. Eng. (FSE-4, 1995.

S. Mcdirmid, W. C. Flatt, and . Hsieh, Jiazzi: New-age components for old-fashioned Java, Proceedings OOPSLA '01, 2001.

N. Medvidovic and R. N. Taylor, A classification and comparison framework for software architecture description languages, IEEE Transactions on Software Engineering, vol.26, issue.1, 2000.
DOI : 10.1109/32.825767
URL : https://hal.archives-ouvertes.fr/hal-00444077

M. Miller, Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control, 2006.

R. Milner, M. Tofte, R. Harper, and D. Macqueen, The Definition of Standard ML (Revised), 1997.

D. Nicola, G. L. Ferrari, and R. Pugliese, KLAIM: a kernel language for agents interaction and mobility, IEEE Transactions on Software Engineering, vol.24, issue.5, 1998.
DOI : 10.1109/32.685256

M. Odersky and M. Zenger, Scalable component abstractions, Proceedings OOPSLA, 2005.
DOI : 10.1145/1094811.1094815
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.176.5313

F. Oquendo, ??-ADL, ACM SIGSOFT Software Engineering Notes, vol.29, issue.3, 2004.
DOI : 10.1145/986710.986728

. Osgi-alliance, OSGI Service Platform ? Core Specification ? Release 4, Version 4, 2006.

D. Rémy, Using, Understanding, and Unraveling the OCaml Language, Applied Semantics. Advanced Lectures, 2002.

J. Riely and M. Hennessy, A typed language for distributed mobile processes, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL, 1998.

A. Rossberg, The Missing Link ? Dynamic Components for ML, Int. Conf. Functional Programming (ICFP), 2006.

P. Van-roy, On the separation of concerns in distributed programming: Application to distribution structure and fault tolerance in Mozart, Int. Workshop on Parallel and Distributed Computing for Symbolic and Irregular Applications (PDSIA). World Scientific, 1999.

P. Van-roy, S. Haridi, P. Brand, G. Smolka, M. Mehl et al., Mobile objects in distributed Oz, ACM Transactions on Programming Languages and Systems, vol.19, issue.5, 1997.
DOI : 10.1145/265943.265972

D. Sangiorgi and D. Walker, The ?-calculus: A Theory of Mobile Processes, 2001.

A. Schmitt and J. B. Stefani, The M-calculus: A Higher-Order Distributed Process Calculus, Proceedings 30th Annual ACM Symposium on Principles of Programming Languages, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00072227

A. Schmitt and J. B. Stefani, The Kell Calculus: A Family of Higher-Order Distributed Process Calculi, Global Computing, 2005.
DOI : 10.1007/3-540-45694-5_19

J. , C. Seco, and L. Caires, A basic model of typed components, European Conf. on Object-Oriented Programming, 2000.

J. , C. Seco, and L. Caires, ComponentJ: The Reference Manual, 2002.

P. Sewell, J. Leifer, K. Wansbrough, M. Allen-willians, F. Zappa-nardelli et al., Acute: High-level programming language design for distributed computation ? Design rationale and language definition, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00070671

P. Sewell, J. Leifer, K. Wansbrough, F. Zappa-nardelli, M. Allen-willians et al., Acute: High-level programming language design for distributed computation, Int. Conf. Functional Programming, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00070671

P. Sewell, J. Leifer, K. Wansbrough, F. Zappa-nardelli, M. Allen-willians et al., Acute: High-level programming language design for distributed computation, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00070671

P. Sewell and J. Vitek, Secure composition of untrusted code: box ??, wrappers, and causality types, Journal of Computer Security, vol.11, issue.2, 2003.
DOI : 10.3233/JCS-2003-11202

M. Shaw and D. Garlan, Software Architecture: Perspectives on an Emerging Discipline, 1996.

T. Sheard and S. L. Jones, Template meta-programming for haskell, SIGPLAN Notices, vol.37, issue.12, 2002.
DOI : 10.1145/636517.636528
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.189.4479

F. Spiessens and P. Van-roy, The Oz-E Project: Design Guidelines for a Secure Multiparadigm Programming Language, Multiparadigm Programming in Mozart/Oz, 2nd International Conference, 2004.
DOI : 10.1007/978-3-540-31845-3_3

G. Stoyle, M. W. Hicks, G. M. Bierman, P. Sewell, and I. Neamtiu, Mutatis mutandis: safe and predictable dynamic software updating, 32nd POPL, 2005.

C. Szyperski, Component Software, 2002.

J. C. Tournier, J. P. Babau, and V. Olive, Qinna, a Component-Based QoS Architecture, CBSE, 2005.
DOI : 10.1007/11424529_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.129.7378

P. Van-roy, Self Management and the Future of Software Design, Electronic Notes in Theoretical Computer Science, vol.182, 2006.
DOI : 10.1016/j.entcs.2006.12.043

P. Van-roy and S. Haridi, Concepts, Techniques and Models of Computer Programming, 2004.

M. Wermelinger and J. Fiadeiro, A graph transformation approach to run-time software architecture reconfiguration, Proceedings ESEC/FSE 1999, 1999.

M. Wermelinger, A. Lopes, and J. Fiadeiro, A Graph Based Architectural (Re)configuration Language, Proceedings ESEC/FSE 2001, 2001.
DOI : 10.1145/503271.503213
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.3692

P. Wojciechowski and P. Sewell, Nomadic Pict: Language and Infrastructure, IEEE Concurrency, vol.8, issue.2, 2000.
DOI : 10.1109/asama.1999.805388
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.2511

N. Yoshida, Channel dependent types for higher-order mobile processes, Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL). ACM, 2004.
DOI : 10.1145/982962.964014

@. In-this-case and =. U. , By induction, we have ? valid

@. In-this-case and T. ?. Un, By induction

@. In-this-case,-?-n, |. , and =. ?. , Since ?n is valid, by induction, the only possibility to make ? invalid would be if (1) ? |= x = v ? x = v , with v 1? v . But since ?n |= x = ?, we have only ? |= x = terminated, and hence property (1) does not hold

@. In-this-case,-?-n, |. , and =. Inth, for some x, ?, ? , and ? = ?n ? x = ? ? ? : thread(w) ? w ? read(w) ? inth(?, ? ), with ? , w ? dom(?n) By induction, ?n is valid. For ? to be invalid one of the following properties from the definition of store invalidity must hold: (1) with x, ? , (3) with ? , w, (6) with ?, ? , or (8) with ?, ? . Now: (1) does not hold since ?n |= x = ?, ?n valid; (3) does not hold since ?n valid and ? |= ? : thread(w) ? read(w); (6) does not hold since ?n valid and ? fresh Hence ? is valid, ) does not hold since ?n valid (and thus ?n |= ? : kell(?, z) for some ?, z), and ? |= ? : thread(w)

@. Pnew-]-proc{ and $. X. , Xn}S end, ?n |= x = ?, for some x, Xi, S, with ? ? dom(?n) Since ?n is valid by induction and ?n |= x = ?, the addition of assertion x = ? does not make property (1) of store invalidity true. Furthermore, since ? is fresh and only the assertion ? : proc{$ X1, Xn}S end is added, p.property

@. Var-]-we-have-?-=-?-n-?-x1, ?. .. Tn, and =. , T U, with xi fresh, and xi reachable only from ? : T . Hence, since (P ) holds of (?n, Tn) by induction, it holds also of

@. We-have-?-n, |. , =. ¬read-tn-=-?-x, =. , T. U. et al., We have v(? : T, ?) ? v(? x = v T , ?n), and (P ) holds of (?n, Tn) by induction. Hence (P ) holds of

I. De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399