{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T04:29:59Z","timestamp":1744086599286,"version":"3.40.3"},"reference-count":39,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T00:00:00Z","timestamp":1744070400000},"content-version":"unspecified","delay-in-days":97,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n\t  <jats:p>We revisit the communication primitive in ambient calculi. Previously, such communication was confined to first-order (FO) mode (e.g., merely names or capabilities of ambients can be sent), local mode (e.g., the communication only occurs inside an ambient), or particular cross-hierarchy mode (e.g., parent-child communication). In this work, we explore further higher-order (HO) communication in ambient calculi. Specifically, such a communication mechanism allows sending a whole piece of a program across the borders of ambients and is the only form of communication that can happen exactly between ambients. Since ambients are basically of HO nature (i.e., those being moved may be ambients themselves), in a sense, it appears more natural to have HO communication than FO communication. We stipulate that communications merely occur between equally positioned ambients in a peer-to-peer fashion (e.g., between sibling ambients). Following this line, we drop the local or other forms of communication that violate this criterion. As the workbench, we work on a variant of Fair Ambients extended with HO communication, FAHO. This variant also strengthens the original version in that entirely real-identity interaction is guaranteed. We study the semantics, bisimulation, and expressiveness of FAHO. Particularly, we provide the operational semantics using a labeled transition system. Over the semantics, we define the bisimulation in line with the standard notion of bisimulation for ambients and prove that the bisimulation equivalence (i.e., bisimilarity) is a congruence. In addition, we demonstrate that bisimilarity coincides with observational congruence (i.e., barbed congruence). Moreover, we show that FAHO can encode a minimal Turing-complete HO calculus and thus is computationally complete.<\/jats:p>","DOI":"10.1017\/s0960129525000015","type":"journal-article","created":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T02:49:29Z","timestamp":1744080569000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["On higher-order communication in ambient calculi"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9713-9751","authenticated-orcid":false,"given":"Xian","family":"Xu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yan","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhihuan","family":"Yao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2025,4,8]]},"reference":[{"key":"S0960129525000015_ref27","unstructured":"Sangiorgi, D. (1993). Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. Phd thesis. LFCS report ECS-LFCS-93-266. Department of Computer Science, University of Edinburgh."},{"key":"S0960129525000015_ref28","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1006\/inco.1996.0096","article-title":"Bisimulation for higher-order process calculi","volume":"131","author":"Sangiorgi","year":"1996","journal-title":"Information and Computation"},{"key":"S0960129525000015_ref35","doi-asserted-by":"crossref","unstructured":"Schmitt, A. and Stefani, J.-B. (2004). The Kell calculus: A family of higher-order distributed process calculi. In: Proceedings of the IST\/FET International Workshop on Global Computing (GC2004), volume 3267 of Lecture Notes in Computer Science, 146\u2013178.","DOI":"10.1007\/978-3-540-31794-4_9"},{"key":"S0960129525000015_ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2012.8"},{"key":"S0960129525000015_ref1","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1017\/S0960129507006226","article-title":"Boxed ambients with communication interfaces","volume":"17","author":"Bonelli","year":"2007","journal-title":"Mathematical Structures in Computer Science"},{"key":"S0960129525000015_ref11","unstructured":"Cruz, L. R. G. and Aguirre, O. O. (2005). A virtual machine for the ambient calculus. In: Proceedings of the 2nd International Conference on Electrical and Electronics Engineering"},{"key":"S0960129525000015_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.10.001"},{"key":"S0960129525000015_ref7","doi-asserted-by":"crossref","unstructured":"Cerone, A. , Hennessy, M. and Merro, M. (2012). Modelling mac-layer communications in wireless systems. In: Proceedings of the Coordination Models and Languages (COORDINATION 2013), Berlin Heidelberg: Springer, 16\u201330.","DOI":"10.1007\/978-3-642-38493-6_2"},{"key":"S0960129525000015_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1119479.1119482"},{"key":"S0960129525000015_ref37","unstructured":"Sun, Y. (2015). Toward a model checker for ambient logic using the process analysis toolkit. Master\u2019s thesis, Department of Computer Science, Bishop\u2019s University, Sherbrooke, Quebec, Canada."},{"key":"S0960129525000015_ref23","volume-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"S0960129525000015_ref39","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1007\/s00236-012-0168-9","article-title":"Distinguishing and relating higher-order and first-order processes by expressiveness","volume":"49","author":"Xu","year":"2012","journal-title":"Acta Informatica"},{"key":"S0960129525000015_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47813-2_18"},{"key":"S0960129525000015_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00075-8"},{"key":"S0960129525000015_ref25","unstructured":"Mylonakis, N. (2017). A graph semantics for a variant of the ambient calculus more adequate for modeling service oriented computing. In: Electronic pre-proceedings of the Eighth International Workshop on Graph Computation Models, article 7, 1\u201313."},{"key":"S0960129525000015_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-007-0038-z"},{"key":"S0960129525000015_ref15","unstructured":"Fu, Y. (2005). Checking Equivalence for Higher Order Processes-a Progress Report. Technical report. BASICS lab. Shanghai Jiao Tong University, Shanghai, China."},{"key":"S0960129525000015_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61604-7_67"},{"key":"S0960129525000015_ref33","volume-title":"The Pi-Calculus: A Theory of Mobile Processes","author":"Sangiorgi","year":"2001"},{"key":"S0960129525000015_ref38","first-page":"1","article-title":"Types for calculus of mobile code applications","volume":"7","author":"Tom\u00e1sek","year":"2007","journal-title":"Acta Electrotechnica et Informatica"},{"key":"S0960129525000015_ref12","unstructured":"Fournet, C. (1998). The Join-Calculus: a calculus for distributed mobile programming. PhD thesis, Ecole Polytechnique, Palaiseau, Nov. INRIA TU-0556. Also available from http:\/\/research.microsoft.com\/\u223cfournet."},{"key":"S0960129525000015_ref32","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Sangiorgi","year":"2012"},{"key":"S0960129525000015_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24999-0_43"},{"key":"S0960129525000015_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596981"},{"key":"S0960129525000015_ref30","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511777110","volume-title":"Introduction to Bisimulation and Coinduction","author":"Sangiorgi","year":"2011"},{"key":"S0960129525000015_ref13","doi-asserted-by":"crossref","unstructured":"Fournet, C. and Gonthier, G. (1996). The reflexive chemical abstract machine and the join-calculus. In: Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201996), 372\u2013385.","DOI":"10.1145\/237721.237805"},{"key":"S0960129525000015_ref10","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2010.335"},{"key":"S0960129525000015_ref17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2015.07.043","article-title":"Theory of interaction","volume":"611","author":"Fu","year":"2015","journal-title":"Theoretical Computer Science"},{"key":"S0960129525000015_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00832-0"},{"key":"S0960129525000015_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2010.02.003"},{"key":"S0960129525000015_ref5","doi-asserted-by":"crossref","unstructured":"Cao, Z. (2013). On the expressiveness of monadic higher order safe ambient calculus. In: Proceedings of the 2013 International Conference on Foundations of Computer Science(ICTMF 2011), 305\u2013312.","DOI":"10.1007\/978-3-642-24999-0_43"},{"key":"S0960129525000015_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45500-0_2"},{"key":"S0960129525000015_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503280"},{"key":"S0960129525000015_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00231-5"},{"key":"S0960129525000015_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.05.001"},{"key":"S0960129525000015_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604136"},{"key":"S0960129525000015_ref26","volume-title":"Advanced Topics in Bisimulation and Coinduction, Chapter Enhancements of the Coinductive Proof Method","author":"Pous","year":"2011"},{"key":"S0960129525000015_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"S0960129525000015_ref31","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D. and Milner, R. (1992). The problem of weak bisimulation up-to. In: Proceedings of CONCUR\u201992, volume 630 of LNCS, Springer Verlag, 32\u201346.","DOI":"10.1007\/BFb0084781"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129525000015","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T02:49:47Z","timestamp":1744080587000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129525000015\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":39,"alternative-id":["S0960129525000015"],"URL":"https:\/\/doi.org\/10.1017\/s0960129525000015","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}],"article-number":"e2"}}