Article

BASS: boxed ambients with safe sessions

Authors:

Pablo Garralda,

Adriana Compagnoni,

Mariangiola Dezani-CiancagliniAuthors Info & Claims

PPDP '06: Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming

Pages 61 - 72

https://doi.org/10.1145/1140335.1140344

Published: 10 July 2006 Publication History

Abstract

We define BASS, a typed boxed ambients calculus with safe sessions. Sessions offer the possibility of using the same channel to transmit information of different types in a prescribed order. A session involves two communicating processes located either within the same ambient or across an ambient boundary. One of the challenges of adding session primitives to a mobile calculus is how to protect sessions from being interrupted by a mobility step. To address this challenge, we introduce a mechanism that prevents an ambient from moving, if there are pending sessions across its boundaryThe main result of our development is that in a well-typed process a communication redex never disappears after a mobility step. In other words, the residual of a communication redex is present in the reduct of the original process enabling a pending session step to be completed. Therefore, we claim that sessions in our calculus are safe.

References

[1]

Torben Amtoft, Assaf J. Kfoury, and Santiago M. Pericas-Geertsen. What are Polymorphically-Typed Ambients? In David Sands, editor, ESOP'01, volume 2028 of LNCS, pages 206--220. Springer-Verlag, 2001.]]

Digital Library

[2]

Torben Amtoft, Henning Makholm, and Joe B. Wells. PolyA: True Type Polymorphism for Mobile Ambients. In Jean-Jacques Lévy, Ernst W. Mayr, and John C. Mitchell, editors, TCS'04, pages 591--604. Kluwer, 2004.]]

[3]

Henk P. Barendregt. The λ Calculus: its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics 103. North-Holland, Amsterdam, revised edition, 1984.]]

[4]

Eduardo Bonelli, Adriana Compagnoni, and Elsa Gunter. Correspondence Assertions for Process Synchronization in Concurrent Communications. Journal of Functional Programming, 15(2):219--248, 2005.]]

Digital Library

[5]

Eduardo Bonelli, Adriana Compagnoni, and Elsa Gunter. Typechecking Safe Process Synchronization. In Julian Rathke, editor, FGUC 2004, volume 138 of ENTCS, pages 3--22. Elsevier, 2005.]]

Digital Library

[6]

Eduardo Bonelli, Adriana B. Compagnoni, Mariangiola Dezani-Ciancaglini, and Pablo Garralda. Boxed Ambients with Communication Interfaces. In Václav Fiala, Jiríand Koubek and Kratochvíl Jan, editors, MFCS'04, volume 3153 of LNCS, pages 119--148. Springer-Verlag, 2004.]]

[7]

Gérard Boudol. A Parametric Model of Migration and Mobility, Release 1. Mikado Deliverable D1.2.1, available at http://mikado.di.fc.ul.pt/repository/D1.2.1.pdf, 2003.]]

[8]

Michele Bugliesi and Giuseppe Castagna. Behavioral Typing for Safe Ambients. Computer Languages, 28(1):61--99, 2002.]]

Digital Library

[9]

Michele Bugliesi, Giuseppe Castagna, and Silvia Crafa. Access Control for Mobile Agents: The Calculus of Boxed Ambients. ACM Transactions on Programming Languages and Systems, 26(1):57--124, 2004.]]

Digital Library

[10]

Michele Bugliesi, Silvia Crafa, Massimo Merro, and Vladimiro Sassone. Communication and Mobility Control in Boxed Ambients. Information and Computation, 202(1):39--86, 2005.]]

Digital Library

[11]

Marco Carbone, Kohei Honda, and Nobuko Yoshida. A Theoretical Basis of Communication-centered Concurrent Programming. Web Services Choreography Working Group mailing list, to appear as a WS-CDL working report.]]

[12]

Luca Cardelli. Abstractions for Mobile Computation. In Jan Vitek and Christian Jensen, editors, Secure Internet Programming, volume 1603 of LNCS, pages 51--94. Springer-Verlag, 1999.]]

Digital Library

[13]

Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon. Mobility Types for Mobile Ambients. In Jiri Wiedermann, Peter van Emde Boas, and Mogens Nielsen, editors, ICALP'99, volume 1644 of LNCS, pages 230--239. Springer-Verlag, 1999.]]

Digital Library

[14]

Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon. Types for the Ambient Calculus. Information and Computation, 177(2):160--194, 2002.]]

Digital Library

[15]

Luca Cardelli and Andrew D. Gordon. Mobile Ambients. Theoretical Computer Science, 240(1):177--213, 2000. Special Issue on Coordination, Daniel Le Métayer Editor.]]

Digital Library

[16]

Giuseppe Castagna, Jan Vitek, and Francesco Zappa Nardelli. The Seal Calculus. Information and Computation, 201(1):1--54, 2005.]]

Digital Library

[17]

Mario Coppo, Mariangiola Dezani-Ciancaglini, Elio Giovannetti, and Rosario Pugliese. Dynamic and Local Typing for Mobile Ambients. In Jean-Jacques Lévy, Ernst W. Mayr, and John C. Mitchell, editors, TCS'04, pages 583--596. Kluwer, 2004.]]

[18]

Mario Coppo, Mariangiola Dezani-Ciancaglini, Elio Giovannetti, and Ivano Salvo. M3: Mobility Types for Mobile Processes in Mobile Ambients. In James Harland, editor, CATS'03, volume 78 of ENTCS. Elsevier, 2003.]]

[19]

Rocco De Nicola, GianLuigi Ferrari, and Rosario Pugliese. Klaim: a Kernel Language for Agents Interaction and Mobility. IEEE Transactions on Software Engineering, 24(5):315--330, 1998.]]

Digital Library

[20]

Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopoulou. Session Types for Object-Oriented Languages. In Dave Thomas, editor, ECOOP'06, volume 4067 of LNCS, pages 328--352. Springer-Verlag, 2006.]]

Digital Library

[21]

Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, Alex Ahern, and Sophia Drossopoulou. A Distributed Object Oriented Language with Session Types. In Rocco De Nicola and Davide Sangiorgi, editors, TGC'05, volume 3705 of LNCS, pages 299--318. Springer-Verlag, 2005.]]

Digital Library

[22]

Pablo Garralda and Adriana Compagnoni. Splitting Mobility and Communication in Boxed Ambients. In Maribel Fernández and Ian Mackie, editors, DCM'05, volume 135 of ENTCS, pages 105--114. Elsevier, 2005.]]

Digital Library

[23]

Simon Gay and Malcolm Hole. Types and Subtypes for Client-Server Interactions. In S. Doaitse Swierstra, editor, ESOP'99, volume 1576 of LNCS, pages 74--90. Springer-Verlag, 1999.]]

Digital Library

[24]

Simon Gay and Malcolm Hole. Subtyping for session types in the pi-calculus. Acta Informatica, 42(2/3):191--225, 2005.]]

[25]

Simon Gay, Vasco T. Vasconcelos, and António Ravara. Session Types for Inter-Process Communication. TR 2003--133, Department of Computing, University of Glasgow, 2003.]]

[26]

Elio Giovannetti. Ambient Calculi with Types: a Tutorial. In Corrado Priami, editor, Global Computing, volume 2874 of LNCS, pages 151--191. Springer-Verlag, 2003.]]

[27]

Andrew D. Gordon and Alan Jeffrey. Typing Correspondence Assertions for Communication Protocols. In Stephen Brooks and Michael Mislove, editors, MFPS'01, volume 45 of ENTCS, pages 379--409. Elsevier, 2001.]]

[28]

Mattew Hennessy and James Riely. Resource Access Control in Systems of Mobile Agents. Information and Computation, 173:82--120, 2002.]]

Digital Library

[29]

Kohei Honda. Types for Dyadic Interaction. In Eike Best, editor, CONCUR'93, volume 715 of LNCS, pages 509--523. Springer-Verlag, 1993.]]

Digital Library

[30]

Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language Primitives and Type Disciplines for Structured Communication-based Programming. In Chris Hankin, editor, ESOP'98, volume 1381 of LNCS, pages 22--138. Springer-Verlag, 1998.]]

Digital Library

[31]

Gérard Huet and Jean-Jacques Lévy. Computations in Orthogonal Rewriting Systems, I. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 395--414. MIT Press, Cambridge, MA, 1991.]]

[32]

Francesca Levi and Davide Sangiorgi. Controlling Interference in Ambients. Transactions on Programming Languages and Systems, 25(1):1--69, 2003.]]

Digital Library

[33]

Cédric Lhoussaine and Vladimiro Sassone. A Dependently Typed Ambient Calculus. In David Schmidt, editor, ESOP'04, volume 2986 of LNCS, pages 171--187. Springer-Verlag, 2004.]]

[34]

Massimo Merro and Matthew Hennessy. Bisimulation Congruences in Safe Ambients. In Neil D. Jones and Xavier Leroy, editors, POPL'02, pages 71--80. ACM Press, 2002.]]

Digital Library

[35]

Massimo Merro and Vladimiro Sassone. Typing and Subtyping Mobility in Boxed Ambients. In Lubos Brim, Petr Jancar, Mojmir Kretinsky, and Antonin Kucera, editors, CONCUR'02, volume 2421 of LNCS, pages 304--320. Springer-Verlag, 2002.]]

Digital Library

[36]

Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An Interaction-based Language and its Typing System. In Constantine Halatsis, Dimitris G. Maritsas, George Philokyprou, and Sergios Theodoridis, editors, PARLE'94, volume 817 of LNCS, pages 398--413. Springer-Verlag, 1994.]]

Digital Library

[37]

Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.]]

[38]

Antonio Vallecillo, Vasco T. Vasconcelos, and António Ravara. Typing the Behavior of Objects and Components using Session Types. In Antonio Brogi and Jean-Marie Jacquet, editors, FOCLASA'02, volume 68(3) of ENTCS. Elsevier, 2002.]]

[39]

Vasco T. Vasconcelos, António Ravara, and Simon Gay. Session types for functional multithreading. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR'04, volume 3170 of LNCS, pages 497--511. Springer-Verlag, 2004.]]

[40]

Web Services Choreography Working Group. Web Services Choreography Description Language. http://www.w3.org/2002/ws/chor/.]]

[41]

ZDNet. 2.3 bln wireless subscribers by 2009, June 2005. http://blogs.zdnet.com/ITFacts/?p=8102.]]

[42]

ZDNet. 866 mln bluetooth devices by 2009, November 2005. http://blogs.zdnet.com/ITFacts/?p=9485.]]

Cited By

Johnsen ESteffen MStumpf J(2020)Assumption-Commitment Types for Resource Management in Virtually Timed AmbientsLeveraging Applications of Formal Methods, Verification and Validation: Verification Principles10.1007/978-3-030-61362-4_6(103-121)Online publication date: 29-Oct-2020
https://doi.org/10.1007/978-3-030-61362-4_6
Tran MBendixen ABojesen BHüttel HLybech SBergenti FCastegren EDe Koster JFranco J(2019)Locations and session types in a language with higher-order reflectionProceedings of the 9th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control10.1145/3358499.3361223(31-40)Online publication date: 22-Oct-2019
https://dl.acm.org/doi/10.1145/3358499.3361223
Honda KYoshida NCarbone M(2016)Multiparty Asynchronous Session TypesJournal of the ACM10.1145/282769563:1(1-67)Online publication date: 3-Mar-2016
https://dl.acm.org/doi/10.1145/2827695
Show More Cited By

Index Terms

BASS: boxed ambients with safe sessions
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation
  1. Formal languages and automata theory
  2. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Typed context awareness Ambient Calculus for pervasive applications
Abstract
The idea of pervasive computing is that information processing will become part of everyday life, and will be available everywhere, making computing so natural to the point of being invisible in the ambient. An important concept that arises with ...
Provably Correct Pervasive Computing Environments
PERCOM '08: Proceedings of the 2008 Sixth Annual IEEE International Conference on Pervasive Computing and Communications

The field of pervasive computing has seen a lot of exciting innovations in the past few years. However, there are currently no mechanisms for describing the properties and capabilities of pervasive computing environments in a formal manner. This makes ...
Session types revisited
PPDP '12: Proceedings of the 14th symposium on Principles and practice of declarative programming

Session types are a formalism to model structured communication-based programming. A session type describes communication by specifying the type and direction of data exchanged between two parties. When session types and session primitives are added to ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

PPDP '06: Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming

July 2006

280 pages

ISBN:1595933883

DOI:10.1145/1140335

General Chair:
Annalisa Bossi
Università Ca' Foscari di Venezia, Italy
,
Program Chair:
Michael Maher
National ICT Australia & University of New South Wales, Australia

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 July 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PPDP06

Sponsor:

PPDP06: Principles and Practice of Declarative Programming

July 10 - 12, 2006

Venice, Italy

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
136
Total Downloads

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

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Johnsen ESteffen MStumpf J(2020)Assumption-Commitment Types for Resource Management in Virtually Timed AmbientsLeveraging Applications of Formal Methods, Verification and Validation: Verification Principles10.1007/978-3-030-61362-4_6(103-121)Online publication date: 29-Oct-2020
https://doi.org/10.1007/978-3-030-61362-4_6
Tran MBendixen ABojesen BHüttel HLybech SBergenti FCastegren EDe Koster JFranco J(2019)Locations and session types in a language with higher-order reflectionProceedings of the 9th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control10.1145/3358499.3361223(31-40)Online publication date: 22-Oct-2019
https://dl.acm.org/doi/10.1145/3358499.3361223
Honda KYoshida NCarbone M(2016)Multiparty Asynchronous Session TypesJournal of the ACM10.1145/282769563:1(1-67)Online publication date: 3-Mar-2016
https://dl.acm.org/doi/10.1145/2827695
Castellani IDezani-Ciancaglini MPérez J(2016)Self-adaptation and secure information flow in multiparty communicationsFormal Aspects of Computing10.1007/s00165-016-0381-328:4(669-696)Online publication date: 1-Jul-2016
https://dl.acm.org/doi/10.1007/s00165-016-0381-3
Coppo MDezani-Ciancaglini MVenneri B(2015)Self-adaptive multiparty sessionsService Oriented Computing and Applications10.1007/s11761-014-0171-99:3-4(249-268)Online publication date: 1-Sep-2015
https://dl.acm.org/doi/10.1007/s11761-014-0171-9
Coppo MDezani-Ciancaglini MVenneri B(2014)Self-Adaptive Monitors for Multiparty SessionsProceedings of the 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing10.1109/PDP.2014.18(688-696)Online publication date: 12-Feb-2014
https://dl.acm.org/doi/10.1109/PDP.2014.18
Di Giusto CPérez J(2013)Session Types with Runtime Adaptation: Overview and ExamplesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.137.3137(21-32)Online publication date: 8-Dec-2013
https://doi.org/10.4204/EPTCS.137.3
Di Giusto CPérez JShin SMaldonado J(2013)Disciplined structured communications with consistent runtime adaptationProceedings of the 28th Annual ACM Symposium on Applied Computing10.1145/2480362.2480716(1913-1918)Online publication date: 18-Mar-2013
https://dl.acm.org/doi/10.1145/2480362.2480716
BETTINI LCAPECCHI SDEZANI-CIANCAGLINI MGIACHINO EVENNERI B(2013)Deriving session and union types for objectsMathematical Structures in Computer Science10.1017/S096012951200088623:06(1163-1219)Online publication date: 9-May-2013
https://doi.org/10.1017/S0960129512000886
Dezani-Ciancaglini MDrossopoulou SMostrous DYoshida N(2009)Objects and session typesInformation and Computation10.1016/j.ic.2008.03.028207:5(595-641)Online publication date: 1-May-2009
https://dl.acm.org/doi/10.1016/j.ic.2008.03.028
Show More Cited By

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten