Article

Logical properties of name restriction

Authors:

Luca Cardelli,

Andrew D. GordonAuthors Info & Claims

TLCA'01: Proceedings of the 5th international conference on Typed lambda calculi and applications

Pages 46 - 60

Published: 02 May 2001 Publication History

Abstract

We extend the modal logic of ambients described in [7] to the full ambient calculus, including name restriction. We introduce logical operators that can be used to make assertions about restricted names, and we study their properties.

References

[1]

Martín Abadi, Secrecy by Typing in Security Protocols. JACM 46, 5 (September 1999), 749-786.

Digital Library

Google Scholar

[2]

Martín Abadi and Andrew D. Gordon, A Calculus for Cryptographic Protocols: the Spi Calculus. Information and Computation 148(1999): 1-70.

Digital Library

Google Scholar

[3]

Luís Caires and Luís Monteiro, Verifiable and Executable Logic Specifications of Concurrent Objects in L_π. In Programming Languages and Systems, Proceedings of ESOP'98, Chris Hankin (Ed.), LNCS, Springer, 1998. pp. 42-56.

Digital Library

Google Scholar

[4]

Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon, Secrecy and Group Creation. Catuscia Palamidessi, editor. Proceedings of CONCUR 2000. LNCS 1877, Springer 2000, pp. 365-379.

Digital Library

Google Scholar

[5]

Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon, Ambient Groups and Mobility Types. Proceedings of IFIP TCS2000. J. van Leeuwen, O. Watanabe, M. Hagiya, ED. Mosses, T. Ito (Eds.). Theoretical Computer Science; Exploring New Frontiers in Theoretical Informatics. LNCS 1872, Springer, 2000. pp. 333-347.

Digital Library

Google Scholar

[6]

Luca Cardelli and Andrew D. Gordon, Mobile Ambients. Foundations of Software Science and Computational Structures, Maurice Nivat (Ed.), LNCS 1378, Springer, 1998. pp. 140-155.

Digital Library

Google Scholar

[7]

Luca Cardelli and Andrew D. Gordon, Anytime, Anywhere. Modal Logics for Mobile Ambients. Proceedings of the 27th ACM Symposium on Principles of Programming Languages, 2000. pp 365-377.

Digital Library

Google Scholar

[8]

Silvano Dal Zilio, Spatial Congruence for Ambients is Decidable. Technical Report MSR-TR-2000- 41, Microsoft Research, May 2000.

Google Scholar

[9]

Furio Honsell, Marino Miculan and Ivan Scangnetto, π-Calculus in (Co)Inductive Type Theory. TCS 2000.

Digital Library

Google Scholar

[10]

Murdoch J. Gabbay and Andrew M. Pitts, A New Approach to Abstract Syntax Involving Binders. In Proceedings 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 1999. IEEE Computer Society Press, 1999. pp 214-224.

Digital Library

Google Scholar

[11]

Andrew D. Gordon and Luca Cardelli, Equational Properties of Mobile Ambients. Wolfgang Thomas, Editor. Foundations of Software Science and Computational Structures, Second International Conference, FOSSACS'99. LNCS 1578. Springer, 1999. pp 212-226.

Digital Library

Google Scholar

[12]

Robin Milner, Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999.

Digital Library

Google Scholar

[13]

Robin Milner, Joachim Parrow and David Walker, A Calculus of Mobile Processes, Parts 1-2. Information and Computation, 100(1), 1-77. 1992

Digital Library

Google Scholar

[14]

Davide Sangiorgi, Extensionality and Intensionality in the Ambient Logics. Proceedings of the 28th ACM Symposium on Principles of Programming Languages, 2001. pp 4-13.

Digital Library

Google Scholar

Cited By

View all

Gabbay MLitak TPetrişan D(2011)Stone duality for nominal Boolean algebras with ИProceedings of the 4th international conference on Algebra and coalgebra in computer science10.5555/2040096.2040112(192-207)Online publication date: 30-Aug-2011
https://dl.acm.org/doi/10.5555/2040096.2040112
Kwiatkowska MNorman GParker DVigliotti M(2009)Probabilistic Mobile AmbientsTheoretical Computer Science10.1016/j.tcs.2008.12.058410:12-13(1272-1303)Online publication date: 20-Mar-2009
https://dl.acm.org/doi/10.1016/j.tcs.2008.12.058
Cervesato IScedrov A(2009)Relating state-based and process-based concurrency through linear logic (full-version)Information and Computation10.1016/j.ic.2008.11.006207:10(1044-1077)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.1016/j.ic.2008.11.006
Show More Cited By

Logical properties of name restriction
1. Theory of computation

Recommendations

A logical framework for reasoning about logical specifications
Computing the Number Restriction Deduced from the Existential Restriction in Description Logic with Primitive Negation, Existential Restriction and Number Restriction
FSKD '08: Proceedings of the 2008 Fifth International Conference on Fuzzy Systems and Knowledge Discovery - Volume 05

In this paper we discuss the relation between the number restriction and existential restriction in description logic ALεN. We show that incompatible existential restrictions on the top conjunction of concept descriptions can deduce a number restriction,...
The logical essence of call-by-name CPS translations
PPDP '24: Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming

Recently, the authors identified the “logical essence” of the call-by-value CPS translation to be its decomposition into two translations: a map into a fragment of the sequent calculus LJQ already determining the same semantics as CPS; and a later, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

TLCA'01: Proceedings of the 5th international conference on Typed lambda calculi and applications

May 2001

429 pages

ISBN:3540419608

Editor:
Samson Abramsky
Oxford University Computing Laboratory, Oxford

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 02 May 2001

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
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

View all

Gabbay MLitak TPetrişan D(2011)Stone duality for nominal Boolean algebras with ИProceedings of the 4th international conference on Algebra and coalgebra in computer science10.5555/2040096.2040112(192-207)Online publication date: 30-Aug-2011
https://dl.acm.org/doi/10.5555/2040096.2040112
Kwiatkowska MNorman GParker DVigliotti M(2009)Probabilistic Mobile AmbientsTheoretical Computer Science10.1016/j.tcs.2008.12.058410:12-13(1272-1303)Online publication date: 20-Mar-2009
https://dl.acm.org/doi/10.1016/j.tcs.2008.12.058
Cervesato IScedrov A(2009)Relating state-based and process-based concurrency through linear logic (full-version)Information and Computation10.1016/j.ic.2008.11.006207:10(1044-1077)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.1016/j.ic.2008.11.006
Calcagno CCardelli LGordon A(2005)Deciding validity in a spatial logic for treesJournal of Functional Programming10.1017/S095679680400540415:4(543-572)Online publication date: 1-Jul-2005
https://dl.acm.org/doi/10.1017/S0956796804005404
Bettini LDe Nicola RLoreti M(2004)Formulae Meet Programs Over the NetAutomated Software Engineering10.1023/B:AUSE.0000028536.34044.4711:3(245-288)Online publication date: 1-Jun-2004
https://dl.acm.org/doi/10.1023/B%3AAUSE.0000028536.34044.47
Caires LCardelli L(2004)A spatial logic for concurrency--IITheoretical Computer Science10.1016/j.tcs.2003.10.041322:3(517-565)Online publication date: 6-Sep-2004
https://dl.acm.org/doi/10.1016/j.tcs.2003.10.041
Dawar AGardner PGhelli G(2004)Adjunct elimination through games in static ambient logicProceedings of the 24th international conference on Foundations of Software Technology and Theoretical Computer Science10.1007/978-3-540-30538-5_18(211-223)Online publication date: 16-Dec-2004
https://dl.acm.org/doi/10.1007/978-3-540-30538-5_18
Moody J(2004)Logical mobility and locality typesProceedings of the 14th international conference on Logic Based Program Synthesis and Transformation10.1007/11506676_5(69-84)Online publication date: 26-Aug-2004
https://dl.acm.org/doi/10.1007/11506676_5

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.

Abstract

References

Cited By

Recommendations

A logical framework for reasoning about logical specifications

Computing the Number Restriction Deduced from the Existential Restriction in Description Logic with Primitive Negation, Existential Restriction and Number Restriction

The logical essence of call-by-name CPS translations

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations