Hostname: page-component-6bf8c574d5-b4m5d Total loading time: 0 Render date: 2025-02-21T22:52:54.239Z Has data issue: false hasContentIssue false
  • English
  • Français

Higher-order psi-calculi†

Published online by Cambridge University Press:  24 June 2013

JOACHIM PARROW ,
JOHANNES BORGSTRÖM ,
PALLE RAABJERG  and
JOHANNES ÅMAN POHJOLA
JOACHIM PARROW
Affiliation:
Department of Information Technology, Uppsala University, Uppsala, Sweden Email: joachim.parrow@it.uu.se; johannes.borgstrom@it.uu.se; palle.raabjerg@it.uu.se; johannes.aman-pohjola@it.uu.se.
JOHANNES BORGSTRÖM
Affiliation:
Department of Information Technology, Uppsala University, Uppsala, Sweden Email: joachim.parrow@it.uu.se; johannes.borgstrom@it.uu.se; palle.raabjerg@it.uu.se; johannes.aman-pohjola@it.uu.se.
PALLE RAABJERG
Affiliation:
Department of Information Technology, Uppsala University, Uppsala, Sweden Email: joachim.parrow@it.uu.se; johannes.borgstrom@it.uu.se; palle.raabjerg@it.uu.se; johannes.aman-pohjola@it.uu.se.
JOHANNES ÅMAN POHJOLA
Affiliation:
Department of Information Technology, Uppsala University, Uppsala, Sweden Email: joachim.parrow@it.uu.se; johannes.borgstrom@it.uu.se; palle.raabjerg@it.uu.se; johannes.aman-pohjola@it.uu.se.
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 24 , Issue 2 , April 2014 , e240203
Copyright
Copyright © Cambridge University Press 2013 

Footnotes

†

This work was partly supported by the Swedish Research Council grant UPMARC.

References

Åman 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.)Google Scholar
Bengtson, J. (2010) Formalising process calculi, Ph.D. thesis, Uppsala University.Google Scholar
Borgström, J., Gutkovas, R., Parrow, J., Victor, B. and Åman Pohjola, J. (2013) A Sorted Semantic Framework for High-Level Concurrency.Google Scholar
Borgström, J.et al. (2011) Broadcast psi-calculi with an application to wireless protocols. In: Barthe, G., Pardo, A. and Schneider, G. (eds.) Proceedings SEFM. Springer-Verlag Lecture Notes in Computer Science 704174–89.Google Scholar
Bengtson, J., Johansson, M., Parrow, J. and Victor, B. (2009) Psi-calculi: Mobile processes, nominal data, and logic. In: Proceedings of LICS 2009, IEEE Computer Society 39–48. (Full version available at http://user.it.uu.se/~joachim/psi-long.pdf.)Google Scholar
Bengtson, J., Johansson, M., Parrow, J. and Victor, B. (2010) Weak equivalences in psi-calculi. In: Proceedings of LICS 2010, IEEE Computer Society 322–331.Google Scholar
Bengtson, J., Johansson, M., Parrow, J. and Victor, B. (2011) Psi-calculi: a framework for mobile processes with nominal data and logic. Logical Methods in Computer Science 7 (1)2011.Google Scholar
Bengtson, J. and Parrow, J. (2009) Psi-calculi in Isabelle. In: Berghofer, S., Nipkow, T., Urban, C. and Wenzel, M. (eds.) Proceedings of TPHOLs 2009. Springer-Verlag Lecture Notes in Computer Science 567499–114.Google Scholar
Demangeon, R., Hirschkoff, D. and Sangiorgi, D. (2009) Termination in higher-order concurrent calculi. In: Arbab, F. and Sirjani, M. (eds.) Proceedings FSEN. Springer-Verlag Lecture Notes in Computer Science 596181–96.Google Scholar
Gabbay, M. and Pitts, A. (2001) A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13 341–363.CrossRefGoogle Scholar
Johansson, M. (2010) Psi-calculi: a framework for mobile process calculi, Ph.D. thesis, Uppsala University.Google Scholar
Jeffrey, A. and Rathke, J. (2005) Contextual equivalence for higher-order pi-calculus revisited. Logical Methods in Computer Science 1 (1).Google Scholar
Johansson, M., Victor, B. and Parrow, J. (2010) A fully abstract symbolic semantics for psi-calculi. In: Proceedings of SOS 2009. Electronic Proceedings in Theoretical Computer Science 1817–31.Google Scholar
Lanese, I., Pérez, J. A., Sangiorgi, D. and Schmitt, A. (2008) On the expressiveness and decidability of higher-order process calculi. In: Proceedings LICS, IEEE Computer Society 145–155.Google Scholar
Lanese, I., Pérez, J. A., Sangiorgi, D. and Schmitt, A. (2010) On the expressiveness of polyadic and synchronous communication in higher-order process calculi. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F. and Spirakis, P. G. (eds.) Proceedings ICALP (2). Springer-Verlag Lecture Notes in Computer Science 6199442–453.Google Scholar
Pitts, A. M. (2003) Nominal logic, a first order theory of names and binding. Information and Computation 186 165–193.CrossRefGoogle Scholar
Sangiorgi, D. (1993) From pi-calculus to higher-order pi-calculus – and back. In: Gaudel, M.-C. and Jouannaud, J.-P. (eds.) Proceedings TAPSOFT. Springer-Verlag Lecture Notes in Computer Science 668151–166.Google Scholar
Sangiorgi, D. (1996) Bisimulation for higher-order process calculi. Information and Computation 131 (2)141–178.CrossRefGoogle Scholar
Sangiorgi, D. (1998) On the bisimulation proof method. Mathematical Structures in Computer Science 8 (5)447–479. (An extended abstract also appeared in the Proceedings of MFCS '95, Springer-Verlag Lecture Notes in Computer Science 969 479–488.)CrossRefGoogle Scholar
Sangiorgi, D. (2001) Asynchronous process calculi: the first- and higher-order paradigms. Theoretical Computer Science 253 (2)311–350.CrossRefGoogle Scholar
Thomsen, B. (1989) A calculus of higher order communicating systems. In: Proceedings POPL, ACM Press 143–154.Google Scholar
Thomsen, B. (1993) Plain CHOCS: A second generation calculus for higher order processes. Acta Informatica 30 (1)1–59.CrossRefGoogle Scholar
Urban, C. (2008) Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning 40 (4)327–356.CrossRefGoogle Scholar