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

Direct link
Formalising process calculi
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Theories of mobile processes)
2010 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

As the complexity of programs increase, so does the complexity of the models required to reason about them. Process calculi were introduced in the early 1980s and have since then been used to model communication protocols of varying size and scope. Whereas modeling sophisticated  protocols in simple process algebras like CCS or the pi-calculus is doable, expressing the models required is often gruesome and error prone. To combat this, more advanced process calculi were introduced, which significantly reduce the complexity of the models. However, this simplicity comes at a price -- the theories of the calculi themselves instead become gruesome and error prone, establishing their mathematical and logical properties has turned out to be difficult. Many of the proposed calculi have later turned out to be inconsistent.

The contribution of this thesis is twofold. First we provide methodologies to formalise the meta-theory of process calculi in an interactive theorem prover. These are used to formalise significant parts of the meta-theory of CCS and the pi-calculus in the theorem prover Isabelle, using Nominal Logic to allow for a smooth treatment of the binders. Second we introduce and formalise psi-calculi, a framework for process calculi incorporating several existing ones, including those we already formalised, and which is significantly simpler and substantially more expressive. Our methods scale well as complexity of the calculi increases.

The formalised results for all calculi include congruence results for both strong and weak bisimilarities, in the case of the pi-calculus for both the early and the late operational semantics. For the finite pi-calculus, we also formalise the proof that the axiomatisation of strong late bisimilarity is sound and complete. We believe psi-calculi to be the state of the art of process calculi, and our formalisation to be the most extensive formalisation of process calculi ever done inside a theorem prover.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis , 2010. , 480 p.
Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1104-2516 ; 93
Keyword [en]
process calculi, interactive theorem proving, nominal logic, pi-calculus, CCS, psi-calculi
National Category
Computer Science
Research subject
Computer Science
URN: urn:nbn:se:uu:diva-122782ISBN: 978-91-554-7801-8OAI: oai:DiVA.org:uu-122782DiVA: diva2:311032
Public defence
2010-06-04, Häggsalen, Ångströmlaboratoriet, Lägerhyddsvägen 1, Uppsala, 10:00 (English)
Available from: 2010-05-12 Created: 2010-04-19 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text
Buy this publication >>

Search in DiVA

By author/editor
Bengtson, Jesper
By organisation
Division of Computer SystemsComputer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
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

Total: 954 hits
ReferencesLink to record
Permanent link

Direct link