No CrossRef data available.
Article contents
Higher-order psi-calculi†
Published online by Cambridge University Press: 24 June 2013
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.
Information
- Type
- Paper
- Information
- 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
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
You have
Access
- 11
- Cited by