{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T20:10:04Z","timestamp":1748549404114,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"5-6","license":[{"start":{"date-parts":[[2015,11,1]],"date-time":"2015-11-01T00:00:00Z","timestamp":1446336000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2015,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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<jats:italic>invisible<\/jats:italic>in the ambient. An important concept that arises with pervasive computing is<jats:italic>context awareness<\/jats:italic>. Context is any information that can be used to characterize an entity. Based on contextual information, applications can dynamically adapt themselves to the environments in which they operate. The Calculus of Context-aware Ambients (CCA) is an untyped formal language used to describe mobile and context-aware pervasive applications. The CCA extends the Ambient Calculus by providing new features, such as context-guarded action and process abstraction, allowing to model contexts and context-aware computations. In this work, we define a type system for the CCA, called<jats:italic>CCA<\/jats:italic><jats:sub><jats:italic>T<\/jats:italic><\/jats:sub>, with the focus in the communication between processes and in the correct use of process abstraction and contexts, extending previous works on the definition of type systems for mobile computing. Moreover, we prove that the proposed type system has the subject reduction property (or type preservation). We also model a hospital scenario using<jats:italic>CCA<\/jats:italic><jats:sub><jats:italic>T<\/jats:italic><\/jats:sub>to demonstrate the use of the proposed type system.<\/jats:p>","DOI":"10.1007\/s00165-015-0339-x","type":"journal-article","created":{"date-parts":[[2015,7,28]],"date-time":"2015-07-28T05:43:56Z","timestamp":1438062236000},"page":"885-916","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Typed context awareness Ambient Calculus for pervasive applications"],"prefix":"10.1145","volume":"27","author":[{"given":"Douglas Pereira","family":"Pasqualin","sequence":"first","affiliation":[{"name":"Centro de Processamento de Dados, Universidade Federal de Santa Maria, Santa Maria, RS, Brazil"}]},{"given":"Juliana Kaizer","family":"Vizzotto","sequence":"additional","affiliation":[{"name":"Departamento de Linguagens e Sistemas de Computa\u00e7\u00e3o, Universidade Federal de Santa Maria, Santa Maria, RS, Brazil"}]},{"given":"Eduardo Kessler","family":"Piveta","sequence":"additional","affiliation":[{"name":"Departamento de Linguagens e Sistemas de Computa\u00e7\u00e3o, Universidade Federal de Santa Maria, Santa Maria, RS, Brazil"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abowd GD Dey AK Brown PJ Davies N Smith M Steggles P (1999) Towards a better understanding of context and context-awareness. In: HUC \u201999: Proceedings of the 1st international symposium on handheld and ubiquitous computing vol 1707 Lecture notes in computer science London UK. Springer Berlin\/Heidelberg pp 304\u2013307","DOI":"10.1007\/3-540-48157-5_29"},{"issue":"6","key":"e_1_2_1_2_2_2","first-page":"329","article-title":"A Java-based programming language support of location management in pervasive systems","volume":"8","author":"Aly SG","year":"2008","journal-title":"Int J Comput Sci Netw Secur"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Augusto JC (2007) Ambient intelligence: the confluence of ubiquitous\/pervasive computing and artificial intelligence. In: Schuster AJ (ed) Intelligent Computing Everywhere chapter 11. Springer London pp 213\u2013234","DOI":"10.1007\/978-1-84628-943-9_11"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/963778.963781"},{"key":"e_1_2_1_2_5_2","unstructured":"Constable RL Allen SF Bromley HM Cleaveland WR Cremer JF Harper RW Howe DJ Knoblock TB Mendler NP Panangaden P Sasaki JT Smith SF (1986) Implementing mathematics with the Nuprl proof development dystem. Prentice-Hall Inc. Upper Saddle River"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/234313.234418"},{"key":"e_1_2_1_2_7_2","unstructured":"Chin JS Callaghan V Clarke G (2006) An end-user programming paradigm for pervasive computing applications. In: ACS\/IEEE international conference on pervasive services pp 325\u2013328"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Coppo M Dezani-Ciancaglini M Giovannetti E Salvo I (2003) M 3 : Mobility types for mobile processes in mobile ambients. Electr Notes Theor Comput Sci 78(0):144\u2013177. CATS\u201903 computing: the Australasian theory symposium","DOI":"10.1016\/S1571-0661(04)81011-9"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Cardelli L Gordon AD (1998) Mobile ambients. In: Proceedings of the first international conference on foundations of software science and computation structure vol 1378. Springer London pp 140\u2013155","DOI":"10.1007\/BFb0053547"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Cardelli L Gordon AD (1999) Types for mobile ambients. In Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL \u201999. ACM New York pp 79\u201392","DOI":"10.1145\/292540.292550"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00231-5"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Charatonik W Gordon A Talbot J-M (2002) Finite-control mobile ambients. In: Le M\u00e9tayer D (ed) Programming languages and systems vol 2305 Lecture notes in computer science . Springer Berlin\/Heidelberg pp 295\u2013313","DOI":"10.1007\/3-540-45927-8_21"},{"key":"e_1_2_1_2_13_2","unstructured":"Dapoigny R Barlatier P (2007) Towards a context theory for context-aware systems. In: Proceeding of the 2007 conference on advances in ambient intelligence. IOS Press Amsterdam pp 36\u201355"},{"key":"e_1_2_1_2_14_2","unstructured":"Deransart P Smaus J-G (2002) Subject reduction of logic programs as proof-theoretic property. J Funct Logic Program 2002"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Grimm R Davis J Hendrickson B Lemar E MacBeth A Swanson S Anderson T Bershad B Borriello G Gribble S Wetherall D (2001) Systems directions for pervasive computing. In: Proceedings of the eighth workshop on hot topics in operating systems 20\u201322 2001. IEEE Computer Society Washington DC pp 147\u2013151","DOI":"10.1109\/HOTOS.2001.990075"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/203043"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in computer science: modelling and reasoning about systems","author":"Huth M","year":"2004"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Hofer T Schwinger W Pichler M Leonhartsberger G Altmann J Retschitzegger W (2003) Context-awareness on mobile devices - the hydrogen approach. In: HICSS \u201903. Proceedings of the 36th Annual Hawaii international conference on system sciences 6\u20139 2003. IEEE Computer Society Washington DC pp 292\u2013302","DOI":"10.1109\/HICSS.2003.1174831"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Julien C Payton J Roman G-C (2004) Reasoning about context-awareness in the presence of mobility. Electron Notes Theor Comput Sci 97(0):259\u2013276. In: Proceedings of FOCLASA 2003 the foundations of coordination languages and software architectures a satellite event of CONCUR 2003.","DOI":"10.1016\/j.entcs.2004.04.040"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Junbin Z Yong Q Di H Min X (2008) Extended isotope programming model for pervasive computing environment. In: Proceedings of the 2008 third international conference on convergence and hybrid information technology ICCIT \u201908 vol 01. IEEE Computer Society Washington DC pp 94\u2013101","DOI":"10.1109\/ICCIT.2008.181"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Junbin Z Yong Q Di H Ming L (2009) A table-driven programming paradigm for context-aware application development. In: IEEE\/IPSJ international symposium on applications and the internet pp 121\u2013124","DOI":"10.1109\/SAINT.2009.27"},{"key":"e_1_2_1_2_22_2","unstructured":"Kj\u00e6rgaard MB Bunde-Pedersen J (2006) Towards a formal model of context awareness. In: Proceedings of the first international workshop on combining theory and systems building in pervasive computing (pervasive 2006) Dublin Ireland pp 667\u2013674"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596981"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Lhoussaine C Sassone V (2004) A dependently typed ambient calculus. In: Schmidt D (ed) Programming languages and systems vol 2986 Lecture notes in computer science . Springer Berlin\/Heidelberg pp 171\u2013187","DOI":"10.1007\/978-3-540-24725-8_13"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Luo Z (2009) Dependent record types revisited. In: Proceedings of the 1st Workshop on modules and libraries for proof assistants MLPA \u201909. ACM New York pp 30\u201337","DOI":"10.1145\/1735813.1735819"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"volume-title":"Communicating and mobile systems: the \u03c0-calculus","year":"1999","author":"Milner R","key":"e_1_2_1_2_27_2"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Min X Jizhong Z Yong Q Hui H Ming L Wei W. Isotope programming model: a kind of program model for context-aware application. In: MUE \u201907: Proceedings of the 2007 international conference on multimedia and ubiquitous engineering. IEEE Computer Society Washington DC pp 597\u2013602","DOI":"10.1109\/MUE.2007.142"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Most\u00e9faoui GK Pasquier-Rocha J Br\u00e9zillon P (2004) Context-aware computing: A guide for the pervasive computing community. In: ICPS \u201904: IEEE\/ACS international conference on pervasive services pp 39\u201348","DOI":"10.1109\/PERSER.2004.1356763"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.024"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Niemela E Latvakoski J (2004) Survey of requirements and solutions for ubiquitous software. In: MUM \u201904: Proceedings of the 3rd international conference on Mobile and ubiquitous multimedia. ACM New York pp 71\u201378","DOI":"10.1145\/1052380.1052391"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Rarau A Benta KI Cremene M (2007) Multifaceted based language for pervasive services with deterministic and fully defined behavior. In: International Conference on Pervasive Services pp 76\u201379","DOI":"10.1109\/PERSER.2007.4283893"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Sangiorgi D (2001) Extensionality and intensionality of the ambient logics. In: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL \u201901. ACM New York pp 4\u201313","DOI":"10.1145\/360204.375707"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Siewe F Cau A Zedan H (2009) CCA: A calculus of context-aware ambients. In: Proceedings of the IEEE 23rd international conference on advanced information networking and applications workshops 2009. WAINA \u201909. May 2009. IEEE Computer Society Bradford pp 972\u2013977","DOI":"10.1109\/WAINA.2009.23"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1185214"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","DOI":"10.1017\/9781316134924","volume-title":"\u03c0-Calculus: a theory of mobile processes","author":"Sangiorgi D","year":"2001"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2010.02.003"},{"key":"e_1_2_1_2_40_2","unstructured":"Weis T Becker C Brandle A (2006) Towards a programming paradigm for pervasive applications based on the ambient calculus. In: International workshop on combining theory and systems building in pervasive computing Dublin Ireland (co-located with Pervasive 2006)"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.1038\/scientificamerican0991-94"},{"key":"e_1_2_1_2_42_2","unstructured":"Wing JM (2002) FAQ on \u03c0-calculus 2002. Microsoft Internal Memo. Accessed April 2012."},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Want R Pering T (2005) System challenges for ubiquitous and pervasive computing. In: ICSE \u201905: Proceedings of the 27th international conference on Software engineering. ACM New York pp 9\u201314","DOI":"10.1145\/1062455.1062463"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646361"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-015-0339-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-015-0339-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-015-0339-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T19:30:28Z","timestamp":1748547028000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-015-0339-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11]]},"references-count":44,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["10.1007\/s00165-015-0339-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-015-0339-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2015,11]]}}}