{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:35:37Z","timestamp":1753889737474,"version":"3.41.2"},"reference-count":15,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2005,4,21]],"date-time":"2005-04-21T00:00:00Z","timestamp":1114041600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"funder":[{"name":"National Science Foundation","award":["0430175"],"award-info":[{"award-number":["0430175"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The higher-order pi-calculus is an extension of the pi-calculus to allow\ncommunication of abstractions of processes rather than names alone. It has been\nstudied intensively by Sangiorgi in his thesis where a characterisation of a\ncontextual equivalence for higher-order pi-calculus is provided using labelled\ntransition systems and normal bisimulations. Unfortunately the proof technique\nused there requires a restriction of the language to only allow finite types.\nWe revisit this calculus and offer an alternative presentation of the labelled\ntransition system and a novel proof technique which allows us to provide a\nfully abstract characterisation of contextual equivalence using labelled\ntransitions and bisimulations for higher-order pi-calculus with recursive types\nalso.<\/jats:p>","DOI":"10.2168\/lmcs-1(1:4)2005","type":"journal-article","created":{"date-parts":[[2005,7,13]],"date-time":"2005-07-13T12:14:40Z","timestamp":1121256880000},"source":"Crossref","is-referenced-by-count":31,"title":["Contextual equivalence for higher-order pi-calculus revisited"],"prefix":"10.46298","volume":"Volume 1, Issue 1","author":[{"given":"Alan","family":"Jeffrey","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julian","family":"Rathke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2005,4,21]]},"reference":[{"doi-asserted-by":"publisher","key":"10.2168\/LMCS-1(1:4)2005_CG98:MobileAmbients","DOI":"10.1007\/BFb0053547"},{"doi-asserted-by":"crossref","unstructured":"C. Fournet and G. Gonthier. A hierarchy of equivalences for asynchronous calculi. InProc. Int. Conf. Automata, Languages and Programming (ICALP), volume 1443 ofLecture Notes in Computer Science. Springer-Verlag, 1998.","key":"10.2168\/LMCS-1(1:4)2005_FournetGonthier:hieeac","DOI":"10.1007\/BFb0055107"},{"doi-asserted-by":"crossref","unstructured":"C. Fournet, G. Gonthier, J-J. Levy, L. Maranget, and D. Remy. A calculus of mobile agents. InProc. CONCUR, volume 1119 ofLecture Notes in Computer Science. Springer-Verlag, 1996.","key":"10.2168\/LMCS-1(1:4)2005_FGLMD96","DOI":"10.1007\/3-540-61604-7_67"},{"doi-asserted-by":"crossref","unstructured":"A. Giacalone, P. Mishra, and S. Prasad. Facile: A symmetric integration of concurrent and functional programming. InProc. TAPSOFT, volume 352 ofLecture Notes in Computer Science, pages 184-209. Springer-Verlag, 1989.","key":"10.2168\/LMCS-1(1:4)2005_GMP89","DOI":"10.1007\/3-540-50940-2_36"},{"doi-asserted-by":"crossref","unstructured":"M. Hennessy and J. Rathke. Typed behavioural equivalences for processes in the presence of subtyping. InProc. Computing: the Australasian Theory Symposium (CATS), Electronic Notes in Theoretical Computer Science. Elsevier, 2002.","key":"10.2168\/LMCS-1(1:4)2005_HR:tbepps02","DOI":"10.1016\/S1571-0661(04)00309-3"},{"doi-asserted-by":"publisher","key":"10.2168\/LMCS-1(1:4)2005_HondaYoshida:Redbps","DOI":"10.1016\/0304-3975(95)00074-7"},{"doi-asserted-by":"crossref","unstructured":"A.S.A Jeffrey and J. Rathke. A theory of bisimulation for a fragment of Concurrent ML with local names. InProc. IEEE Symp. Logic in Computer Science (LICS), pages 311-321. Computer Society Press, 2000.","key":"10.2168\/LMCS-1(1:4)2005_JeffreyRathke:tbcmlln","DOI":"10.1109\/LICS.2000.855780"},{"doi-asserted-by":"crossref","unstructured":"A.S.A Jeffrey and J. Rathke. A fully abstract may testing semantics for concurrent objects. InProc. IEEE Symp. Logic in Computer Science (LICS), pages 101-112. Computer Society Press, 2002.","key":"10.2168\/LMCS-1(1:4)2005_JeffreyRathke:famtsco","DOI":"10.1109\/LICS.2002.1029820"},{"doi-asserted-by":"crossref","unstructured":"J. Riely and M. Hennessy. A typed language for distributed mobile processes. InProc. ACM Conf. Principles of Programming Languages (POPL). ACM Press, 1998.","key":"10.2168\/LMCS-1(1:4)2005_RH98:TypedLanguage","DOI":"10.1145\/268946.268978"},{"unstructured":"D. Sangiorgi.Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh, 1993.","key":"10.2168\/LMCS-1(1:4)2005_SangiorgiThesis"},{"doi-asserted-by":"publisher","key":"10.2168\/LMCS-1(1:4)2005_San96a:BisimulationHOPC","DOI":"10.1006\/inco.1996.0096"},{"doi-asserted-by":"crossref","unstructured":"D. Sangiorgi and R. Milner. On the problem of `weak bisimulation up to'. InProc. CONCUR, volume 630 ofLecture Notes in Computer Science, pages 32-46. Springer-Verlag, 1992.","key":"10.2168\/LMCS-1(1:4)2005_SM92:ProblemWeak","DOI":"10.1007\/BFb0084781"},{"year":"2001","author":"Sangiorgi","key":"10.2168\/LMCS-1(1:4)2005_SangiorgiBook"},{"doi-asserted-by":"crossref","unstructured":"B. Thomsen.Calculi for Higher-Order Communicating Systems. PhD thesis, University of London, 1990.","key":"10.2168\/LMCS-1(1:4)2005_Thom90","DOI":"10.1145\/75277.75290"},{"doi-asserted-by":"crossref","unstructured":"J. Vitek and G. Castagna. Seal: A framework for secure mobile computations. InInternet Programming Languages, volume 1686 ofLecture Notes in Computer Science. Springer-Verlag, 1999.","key":"10.2168\/LMCS-1(1:4)2005_VC99:Seal","DOI":"10.1007\/3-540-47959-7_3"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2274\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2274\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:11:18Z","timestamp":1681243878000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2274"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,4,21]]},"references-count":15,"URL":"https:\/\/doi.org\/10.2168\/lmcs-1(1:4)2005","relation":{"is-same-as":[{"id-type":"arxiv","id":"cs\/0503067","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0503067","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/978-3-642-19718-5_19","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2005,4,21]]},"article-number":"2274"}}