Article

Equational Properties of Mobile Ambients

Authors:

Andrew D. Gordon,

Luca CardelliAuthors Info & Claims

FoSSaCS '99: Proceedings of the Second International Conference on Foundations of Software Science and Computation Structure, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99

Pages 212 - 226

Published: 22 March 1999 Publication History

Abstract

The ambient calculus is a process calculus for describing mobile computation. We develop a theory of Morris-style contextual equivalence for proving properties of mobile ambients. We prove a context lemma that allows derivation of contextual equivalences by considering contexts of a particular limited form, rather than all arbitrary contexts. We give an activity lemma that characterizes the possible interactions between a process and a context. We prove several examples of contextual equivalence. The proofs depend on characterizing reductions in the ambient calculus in terms of a labelled transition system.

References

[1]

M. Abadi, C. Fournet, and G. Gonthier. Secure implementation of channel abstractions. In Proceedings LICS'98, pages 105-116, 1998.

[2]

M. Abadi and A. D. Gordon. A calculus for cryptographic protocolsff The spi calculus. Information and Computation. To appear. An extended version appears as Digital Equipment Corporation Systems Research Center report No. 149, January 1998.

[3]

R. M. Amadio. An asynchronous model of locality, failure, and process mobility. In Proceedings COORDINATION 97, volume 1282 of Lecture Notes in Computer Science. Springer-Verlag, 1997.

[4]

R. M. Amadio and S. Prasad. Localities and failures. In Proceedings FST&TCS'94, volume 880 of Lecture Notes in Computer Science, pages 205-216. Springer-Verlag, 1994.

[5]

G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96(1):217-248, April 1992.

[6]

L. Cardelli and A. D. Gordon. Mobile ambients. In Proceedings FoSSaCS'98, volume 1378 of Lecture Notes in Computer Science, pages 140-155. Springer-Verlag, 1998.

[7]

L. Cardelli and A. D. Gordon. Types for mobile ambients. In Proceedings POPL'99, 1999. To appear.

[8]

R. De Nicola and M. C. B. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83-133, 1984.

[9]

R. Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science, 4:1-23, 1997.

[10]

R. Milner. The polyadic π-calculusff A tutorial. Technical Report ECS-LFCS-91 180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, October 1991.

[11]

R. Milner. The π-calculus. Undergraduate lecture notes, Cambridge University, 1995.

[12]

R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts I and II. Information and Computation, 100:1-40 and 41-77, 1992.

[13]

R. Milner and D. Sangiorgi. Barbed bisimulation. In Proceedings ICALP'92, volume 623 of Lecture Notes in Computer Science. Springer-Verlag, 1992.

[14]

J. H. Morris. Lambda-Calculus Models of Programming Languages. PhD thesis, MIT, December 1968.

[15]

G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223-255, 1997.

[16]

J. Riely and M. Hennessy. A typed language for distributed mobile processes. In Proceedings POPL'98, pages 378-390, 1998.

[17]

D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh, 1992. Available as Technical Report CST-99-93, Computer Science Department, University of Edinburgh.

Cited By

Sewell PWojciechowski PUnyapoth A(2010)Nomadic pictACM Transactions on Programming Languages and Systems10.1145/1734206.173420932:4(1-63)Online publication date: 22-Apr-2010
https://dl.acm.org/doi/10.1145/1734206.1734209
Pene LAdi K(2006)A Calculus for Distributed Firewall Specification and VerificationProceedings of the 2006 conference on New Trends in Software Methodologies, Tools and Techniques: Proceedings of the fifth SoMeT_0610.5555/1565321.1565346(301-315)Online publication date: 28-May-2006
https://dl.acm.org/doi/10.5555/1565321.1565346
Merro MHennessy M(2006)A bisimulation-based semantic theory of Safe AmbientsACM Transactions on Programming Languages and Systems10.1145/1119479.111948228:2(290-330)Online publication date: 1-Mar-2006
https://dl.acm.org/doi/10.1145/1119479.1119482
Show More Cited By

Equational Properties of Mobile Ambients
1. Networks
  1. Network types
2. Theory of computation

Recommendations

Equational properties of mobile ambients

The ambient calculus is a process calculus for describing mobile computation. We develop a theory of Morris-style contextual equivalence for proving properties of mobile ambients. We prove a context lemma that allows derivation of contextual ...
Second-order equational logic
CSL'10/EACSL'10: Proceedings of the 24th international conference/19th annual conference on Computer science logic

We extend universal algebra and its equational logic from first to second order as follows. 1. We consider second-order equational presentations as specified by identities between second-order terms, with both variables and parameterised metavariables ...
The Decidability of Model Checking Mobile Ambients
CSL '01: Proceedings of the 15th International Workshop on Computer Science Logic

The ambient calculus is a formalism for describing the mobility of both software and hardware. The ambient logic is a modal logic designed to specify properties of distributed and mobile computations programmed in the ambient calculus. In this paper we ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FoSSaCS '99: Proceedings of the Second International Conference on Foundations of Software Science and Computation Structure, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99

March 1999

321 pages

ISBN:3540657193

Editor:
Wolfgang Thomas

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 22 March 1999

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sewell PWojciechowski PUnyapoth A(2010)Nomadic pictACM Transactions on Programming Languages and Systems10.1145/1734206.173420932:4(1-63)Online publication date: 22-Apr-2010
https://dl.acm.org/doi/10.1145/1734206.1734209
Pene LAdi K(2006)A Calculus for Distributed Firewall Specification and VerificationProceedings of the 2006 conference on New Trends in Software Methodologies, Tools and Techniques: Proceedings of the fifth SoMeT_0610.5555/1565321.1565346(301-315)Online publication date: 28-May-2006
https://dl.acm.org/doi/10.5555/1565321.1565346
Merro MHennessy M(2006)A bisimulation-based semantic theory of Safe AmbientsACM Transactions on Programming Languages and Systems10.1145/1119479.111948228:2(290-330)Online publication date: 1-Mar-2006
https://dl.acm.org/doi/10.1145/1119479.1119482
Ciaffaglione AHennessy MRathke J(2005)Proof methodologies for behavioural equivalence in DPIProceedings of the 25th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems10.1007/11562436_25(335-350)Online publication date: 2-Oct-2005
https://dl.acm.org/doi/10.1007/11562436_25
Bugliesi MCastagna GCrafa S(2004)Access control for mobile agentsACM Transactions on Programming Languages and Systems10.1145/963778.96378126:1(57-124)Online publication date: 1-Jan-2004
https://dl.acm.org/doi/10.1145/963778.963781
Levi FSangiorgi D(2003)Mobile safe ambientsACM Transactions on Programming Languages and Systems10.1145/596980.59698125:1(1-69)Online publication date: 1-Jan-2003
https://dl.acm.org/doi/10.1145/596980.596981
Zilio S(2001)Mobile processesModeling and verification of parallel processes10.5555/766794.766806(206-222)Online publication date: 1-Jan-2001
https://dl.acm.org/doi/10.5555/766794.766806
Cardelli LGordon A(2001)Logical properties of name restrictionProceedings of the 5th international conference on Typed lambda calculi and applications10.5555/1754621.1754631(46-60)Online publication date: 2-May-2001
https://dl.acm.org/doi/10.5555/1754621.1754631
Cardelli LGordon AWegman MReps T(2000)Anytime, anywhereProceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/325694.325742(365-377)Online publication date: 5-Jan-2000
https://dl.acm.org/doi/10.1145/325694.325742
Levi FSangiorgi DWegman MReps T(2000)Controlling interference in ambientsProceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/325694.325741(352-364)Online publication date: 5-Jan-2000
https://dl.acm.org/doi/10.1145/325694.325741

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents