{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,15]],"date-time":"2026-05-15T00:23:32Z","timestamp":1778804612468,"version":"3.51.4"},"reference-count":23,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2013,6,24]],"date-time":"2013-06-24T00:00:00Z","timestamp":1372032000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2014,4]]},"abstract":"<jats:p>In earlier work we explored the expressiveness and algebraic theory Psi-calculi, which form a parametric framework for extensions of the pi-calculus. In the current paper we consider higher-order psi-calculi through a technically surprisingly simple extension of the framework, and show how an arbitrary psi-calculus can be lifted to its higher-order counterpart in a canonical way. We illustrate this with examples and establish an algebraic theory of higher-order psi-calculi. The formal results are obtained by extending our proof repositories in Isabelle\/Nominal.<\/jats:p>","DOI":"10.1017\/s0960129513000170","type":"journal-article","created":{"date-parts":[[2013,6,24]],"date-time":"2013-06-24T08:14:44Z","timestamp":1372061684000},"source":"Crossref","is-referenced-by-count":11,"title":["Higher-order psi-calculi"],"prefix":"10.1017","volume":"24","author":[{"given":"JOACHIM","family":"PARROW","sequence":"first","affiliation":[]},{"given":"JOHANNES","family":"BORGSTR\u00d6M","sequence":"additional","affiliation":[]},{"given":"PALLE","family":"RAABJERG","sequence":"additional","affiliation":[]},{"given":"JOHANNES","family":"\u00c5MAN POHJOLA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2013,6,24]]},"reference":[{"key":"S0960129513000170_ref6","first-page":"322","volume-title":"Proceedings of LICS 2010","author":"Bengtson","year":"2010"},{"key":"S0960129513000170_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"S0960129513000170_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/BF01200262"},{"key":"S0960129513000170_ref11","unstructured":"Johansson M. (2010) Psi-calculi: a framework for mobile process calculi, Ph.D. thesis, Uppsala University."},{"key":"S0960129513000170_ref21","first-page":"143","volume-title":"Proceedings POPL","author":"Thomsen","year":"1989"},{"key":"S0960129513000170_ref18","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0096"},{"key":"S0960129513000170_ref3","unstructured":"Borgstr\u00f6m J. , Gutkovas R. , Parrow J. , Victor B. and \u00c5man Pohjola J. (2013) A Sorted Semantic Framework for High-Level Concurrency."},{"key":"S0960129513000170_ref17","first-page":"151","volume-title":"Proceedings TAPSOFT","author":"Sangiorgi","year":"1993"},{"key":"S0960129513000170_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"S0960129513000170_ref13","first-page":"17","volume-title":"Proceedings of SOS 2009","author":"Johansson","year":"2010"},{"key":"S0960129513000170_ref1","unstructured":"\u00c5man Pohjola J. and Raabjerg P. (2012) Isabelle proofs for higher-order psi-calculi. Proof scripts for higher-order psi-calculi. (Available at http:\/\/www.it.uu.se\/research\/group\/mobility\/theorem\/hopsi.tar.gz.)"},{"key":"S0960129513000170_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"S0960129513000170_ref9","first-page":"81","volume-title":"Proceedings FSEN","author":"Demangeon","year":"2009"},{"key":"S0960129513000170_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00097-9"},{"key":"S0960129513000170_ref4","first-page":"74","volume-title":"Proceedings SEFM","author":"Borgstr\u00f6m","year":"2011"},{"key":"S0960129513000170_ref2","unstructured":"Bengtson J. (2010) Formalising process calculi, Ph.D. thesis, Uppsala University."},{"key":"S0960129513000170_ref19","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"S0960129513000170_ref8","first-page":"99","volume-title":"Proceedings of TPHOLs 2009","author":"Bengtson","year":"2009"},{"key":"S0960129513000170_ref14","first-page":"145","volume-title":"Proceedings LICS","author":"Lanese","year":"2008"},{"key":"S0960129513000170_ref5","first-page":"39","volume-title":"Proceedings of LICS 2009","author":"Bengtson","year":"2009"},{"key":"S0960129513000170_ref12","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(1:4)2005"},{"key":"S0960129513000170_ref7","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(1:11)2011"},{"key":"S0960129513000170_ref15","first-page":"442","volume-title":"Proceedings ICALP (2)","author":"Lanese","year":"2010"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129513000170","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T21:27:31Z","timestamp":1555968451000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129513000170\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,24]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["S0960129513000170"],"URL":"https:\/\/doi.org\/10.1017\/s0960129513000170","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,6,24]]},"article-number":"e240203"}}