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
Bells and Whistles: Advanced language features in psi-calculi
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computing Science. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
2013 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine-checked proofs of standard algebraic and congruence properties of bisimilarity apply to every instance of the framework.

The contribution of this licentiate thesis is to significantly extend the applicability and expressiveness of psi-calculi by incorporating several advanced language features into the framework: broadcasts, higher-order communication, generalised pattern matching, sorts and priorities. The extensions present several interesting technical challenges, such as negative premises. The machine-checked proofs for standard results about bisimilarity are generalised to each of these new settings, and the proof scripts are freely available online.

Place, publisher, year, edition, pages
Uppsala University, 2013.
Series
Information technology licentiate theses: Licentiate theses from the Department of Information Technology, ISSN 1404-5117 ; 2013-004
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-227638OAI: oai:DiVA.org:uu-227638DiVA: diva2:730682
Supervisors
Projects
UPMARC
Available from: 2013-10-04 Created: 2014-06-29 Last updated: 2017-08-31Bibliographically approved
List of papers
1. Broadcast psi-calculi with an application to wireless protocols
Open this publication in new window or tab >>Broadcast psi-calculi with an application to wireless protocols
Show others...
2015 (English)In: Software and Systems Modeling, ISSN 1619-1366, E-ISSN 1619-1374, Vol. 14, no 1, 201-216 p.Article in journal (Refereed) Published
Abstract [en]

Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. In this paper we add primitives for broadcast communication in order to model wireless protocols. The additions preserve the purity of the psi-calculi semantics, and we formally prove the standard congruence and structural properties of bisimilarity. We demonstrate the expressive power of broadcast psi-calculi by modelling the wireless ad-hoc routing protocol LUNAR and verifying a basic reachability property.

Place, publisher, year, edition, pages
Springer, 2015
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-205258 (URN)10.1007/s10270-013-0375-z (DOI)000349026100012 ()
Projects
UPMARCProFuN
Funder
Swedish Research Council, 2013-4853
Available from: 2013-11-08 Created: 2013-08-15 Last updated: 2017-12-06Bibliographically approved
2. Higher-order psi-calculi
Open this publication in new window or tab >>Higher-order psi-calculi
2014 (English)In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 24, no 2, e240203Article in journal (Refereed) Published
Abstract [en]

Psi-calculi is a parametric framework for extensions of the pi-calculus; in earlier work we have explored their expressiveness and algebraic theory. In this 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.

Place, publisher, year, edition, pages
Cambridge University Press, 2014
Keyword
process calculi, psi calculi, isabelle, theorem proving, nominal, higher-order
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-183610 (URN)10.1017/S0960129513000170 (DOI)000343643500003 ()
Projects
UPMARCProFuN
Funder
Swedish Foundation for Strategic Research
Available from: 2013-06-24 Created: 2012-10-30 Last updated: 2017-12-07Bibliographically approved
3. A Sorted Semantic Framework for Applied Process Calculi (extended abstract)
Open this publication in new window or tab >>A Sorted Semantic Framework for Applied Process Calculi (extended abstract)
Show others...
2014 (English)In: Trustworthy Global Computing: TGC 2013, Springer Berlin/Heidelberg, 2014, 103-118 p.Conference paper, Published paper (Refereed)
Abstract [en]

Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus,  are extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms.

Our goal is a unified framework to represent different process calculi and notions of computation. To this end, we extend our previous work on psi-calculi with novel abstract patterns and pattern matching, and add sorts to the data term language, giving sufficient criteria for subject reduction to hold. Our framework can accommodate several existing process calculi; the resulting transition systems are isomorphic to the originals up to strong bisimulation. We also demonstrate  different notions of computation on data terms, including cryptographic primitives and a lambda-calculus with erratic choice. Substantial parts of the meta-theory of sorted psi-calculi have been machine-checked using Nominal Isabelle.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2014
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8358
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-203382 (URN)10.1007/978-3-319-05119-2_7 (DOI)978-3-319-05118-5 (ISBN)
Conference
8th International Symposium on Trustworthy Global Computing, August 30-31, 2013, Buenos Aires, Argentina
Projects
UPMARCProFuN
Funder
Swedish Foundation for Strategic Research , RIT08­0065
Available from: 2014-03-08 Created: 2013-07-09 Last updated: 2016-02-25
4. Negative premises in applied process calculi
Open this publication in new window or tab >>Negative premises in applied process calculi
Show others...
2013 (English)Report (Other academic)
Series
Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2013-014
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-229004 (URN)
Available from: 2013-06-20 Created: 2014-07-25 Last updated: 2014-07-25Bibliographically approved
5. Bisimulation up-to techniques for psi-calculi
Open this publication in new window or tab >>Bisimulation up-to techniques for psi-calculi
2016 (English)In: Proc. 5th ACM SIGPLAN Conference on Certified Programs and Proofs / [ed] Avigad, J; Chlipala, A, New York: ACM Press, 2016, 142-153 p.Conference paper, Published paper (Refereed)
Abstract [en]

Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine-checked proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework. Bisimulation up-to techniques are methods for reducing the size of relations needed in bisimulation proofs. In this paper, we show how these bisimulation proof methods can be adapted to psi-calculi. We formalise all our definitions and theorems in Nominal Isabelle, and show examples where the use of up to-techniques yields drastically simplified proofs of known results. We also prove new structural laws about the replication operator.

Place, publisher, year, edition, pages
New York: ACM Press, 2016
Keyword
Bisimulation up-to, process calculus, psi-calculi, Isabelle, Nominal Isabelle, nominal logic
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-229008 (URN)10.1145/2854065.2854080 (DOI)000389021600016 ()9781450341271 (ISBN)
Conference
CPP 2016, January 18–19, Saint Petersburg, FL
Available from: 2016-01-18 Created: 2014-07-25 Last updated: 2017-01-24Bibliographically approved

Open Access in DiVA

fulltext(1570 kB)223 downloads
File information
File name FULLTEXT01.pdfFile size 1570 kBChecksum SHA-512
2244018bf3ea1e5f57e32077d0b9bac542e5f8c5cade178ccd6769950997f3fa4461363529bba806f3ebdfc2fa495521ee3346f5491375700590572fbe764e20
Type fulltextMimetype application/pdf

Authority records BETA

Åman Pohjola, Johannes

Search in DiVA

By author/editor
Åman Pohjola, Johannes
By organisation
Division of Computing ScienceComputing Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 223 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 603 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