uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Psi-calculi: Mobile processes, nominal data, and logic
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)ORCID iD: 0000-0003-0174-9032
2009 (English)In: Proc. 24th Annual IEEE Symposium on Logic in Computer Science, Piscataway, NJ: IEEE , 2009, 39-48 p.Conference paper, Published paper (Refereed)
Abstract [en]

A psi-calculus is an extension of the pi-calculus with nominal data types for data structures and for logical assertions representing facts about data. These can be transmitted between processes and their names can be statically scoped using the standard pi-calculus mechanism to allow for scope migrations.

Other proposed extensions of pi can be formulated as psi-calculi; examples include the applied pi-calculus, the spi-calculus, the fusion calculus, the concurrent constraint pi-calculus, and calculi with polyadic communication channels or pattern matching. Psi-calculi can be even more general, for example by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and a predicate logic for assertions.

Our labelled operational semantics and definition of bisimulation is straightforward, without a  structural congruence. We establish minimal requirements on the nominal data and logic in order to prove general algebraic properties of psi-calculi. The proofs are transparent enough to be checked in the interactive proof checker Isabelle.

We are the first to formulate a truly compositional labelled operational semantics for calculi of this caliber. Expressiveness and therefore modelling convenience significantly exceeds that of other formalisms, while the purity of the semantics is on par with the original pi-calculus.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE , 2009. 39-48 p.
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-99783DOI: 10.1109/LICS.2009.20ISI: 000275054800004ISBN: 978-0-7695-3746-7 (print)OAI: oai:DiVA.org:uu-99783DiVA: diva2:208739
Conference
24th Annual IEEE Symposium on Logic in Computer Science (LICS 2009), Los Angeles, CA, AUG 11-14, 2009
Projects
UPMARCProFun
Available from: 2009-03-19 Created: 2009-03-19 Last updated: 2016-02-25

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Bengtson, JesperJohansson, MagnusParrow, JoachimVictor, Björn

Search in DiVA

By author/editor
Bengtson, JesperJohansson, MagnusParrow, JoachimVictor, Björn
By organisation
Computing Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 950 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf