Abstract
Aim of this paper is to develop a filter model for a calculus with mobility and higher-order value passing. We will define it for an extension of the Ambient Calculus in which processes can be passed as values. This model turns out to be fully abstract with respect to the notion of contextual equivalence where the observables are ambients at top level.
Partially supported by MURST Cofin’00 AITCFA Project, MURST Cofin’01 COMETA Project, IST-2001-33477 DART Project and IST-2001-322222 MIKADO Project.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51(1–2):1–77, 1991.
S. Abramsky and C.-H. L. Ong. Full abstraction in the lazy lambda calculus. Information and Computation, 105(2):159–267, 1993.
T. Amtoft, A. J. Kfoury, and S. M. Pericas-Geertsen. What are polymorphically-typed ambients? In ESOP’01, volume 2028 of LNCS, pages 206–220, Berlin, 2001. Springer-Verlag.
H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The Journal of Symbolic Logic, 48(4):931–940, 1983.
G. Boudol. Lambda-calculi for (strict) parallel functions. Information and Computation, 108(1):51–127, 1994.
M. Bugliesi and G. Castagna. Secure safe ambients. In POPL’01, pages 222–235, New York, 2001. ACM Press.
L. Cardelli, G. Ghelli, and A. D. Gordon. Mobility types for mobile ambients. In ICALP’99, volume 1644 of LNCS, pages 230–239, Berlin, 1999. Springer-Verlag.
L. Cardelli and A. D. Gordon. Mobile ambients. In FoSSaCS’98, volume 1378 of LNCS, pages 140–155, Berlin, 1998. Springer-Verlag.
L. Cardelli and A. D. Gordon. Types for mobile ambients. In POPL’99, pages 79–92, New York, 1999. ACM Press.
L. Cardelli and A. D. Gordon. Anytime, anywhere. modal logics for mobile ambients. In POPL’00, pages 365–377, New York, 2000. ACM Press.
M. Coppo and M. Dezani-Ciancaglini. A fully abstract model for mobile ambients. In TOSCA’01, volume 62 of ENTCS. Elsevier Science, 200X. to appear.
F. Damiani, M. Dezani-Ciancaglini, and P. Giannini. A filter model for mobile processes. Mathematical Structures in Computer Science, 9(1):63–101, 1999.
P. Degano, F. Levi, and C. Bodei. Safe ambients: Control flow analysis and security. In ASIAN’00, volume 1961 of LNCS, pages 199–214, Berlin, 2000. Springer-Verlag.
M. Dezani-Ciancaglini, U. de'Liguoro, and A. Piperno. Finite models for conjunctivedisjunctive λ-calculi. Theoretical Computer Science, 170(1–2):83–128, 1996.
M. Dezani-Ciancaglini, U. de'Liguoro, and A. Piperno. A filter model for concurrent λ-calculus. SIAM Journal on Computing, 27(5):1376–1419, 1998.
M. Dezani-Ciancaglini and S. Ghilezan. A lambda model characterizing computational behaviors of terms. In RPC’01, pages 100–118. Tohoku University, 2001.
M. Dezani-Ciancaglini and I. Salvo. Security types for safe mobile ambients. In ASIAN’00, volume 1961 of LNCS, pages 215–236, Berlin, 2000. Springer-Verlag.
A. D. Gordon and L. Cardelli. Equational properties of mobile ambients. In FoSSaCS’99, volume 1578 of LNCS, pages 212–226, Berlin, 1999. Springer-Verlag.
R. R. Hansen, J. G. Jensen, F. Nielson, and H. R. Nielson. Abstract interpretation of mobile ambients. In SAS’99, number 1694 in LNCS, pages 134–148, Berlin, 1999. Springer-Verlag.
C. Hartonas and M. Hennessy. Full abstractness for a functional/concurrent language with higher-order value-passing. Information and Computation, 145(1):64–106, 1998.
M. Hennessy. A fully abstract denotational model for higher-order processes. Information and Computation, 112(1):55–95, 1994.
M. Hennessy. Higher-order process and their models. In ICALP’94, volume 820 of LNCS, pages 286–303, Berlin, 1994. Springer-Verlag.
C.-H. L. Ong. Non-determinism in a functional setting. In LICS’93, pages 275–286, Montreal, Canada, 1993. IEEE Computer Society Press.
D. Sangiorgi. Extensionality and intensionality of the ambient logic. In POPL’01, pages 4–13, New York, 2001. ACM Press.
D. S. Scott. Domains for denotational semantics. In ICALP’82, volume 140 of LNCS, pages 577–613, Berlin, 1982. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coppo, M., Dezani-Ciancaglini, M. (2002). A Fully Abstract Model for Higher-Order Mobile Ambients. In: Cortesi, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2002. Lecture Notes in Computer Science, vol 2294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47813-2_18
Download citation
DOI: https://doi.org/10.1007/3-540-47813-2_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43631-7
Online ISBN: 978-3-540-47813-3
eBook Packages: Springer Book Archive