Extending psi-calculi and their formal proofs
Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. This thesis presents broadcast psi-calculi and higher-order psi-calculi, two extensions of the psi-calculi framework, allowing respectively one-to-many...
Main Author: | |
---|---|
Format: | Others |
Language: | English |
Published: |
Uppsala universitet, Avdelningen för datalogi
2012
|
Subjects: | |
Online Access: | http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-183614 |
id |
ndltd-UPSALLA1-oai-DiVA.org-uu-183614 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-UPSALLA1-oai-DiVA.org-uu-1836142018-01-12T05:09:28ZExtending psi-calculi and their formal proofsengRaabjerg, PalleUppsala universitet, Avdelningen för datalogiUppsala universitet, Datalogi2012Computer SciencesDatavetenskap (datalogi)Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. This thesis presents broadcast psi-calculi and higher-order psi-calculi, two extensions of the psi-calculi framework, allowing respectively one-to-many communications and the use of higher-order process descriptions through conditions in the parameterised logic. Both extensions preserve the purity of the psi-calculi semantics; the standard congruence and structural properties of bisimilarity are proved formally in Isabelle. The work going into the extensions show that depending on the specific extension, working out the formal proofs can be a work-intensive process. We find that some of this work could be automated, and implementing such automation may facilitate the development of future extensions to the psi-calculi framework. UPMARCLicentiate thesis, comprehensive summaryinfo:eu-repo/semantics/masterThesistexthttp://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-183614IT licentiate theses / Uppsala University, Department of Information Technology, 1404-5117 ; 2012-008application/pdfinfo:eu-repo/semantics/openAccess |
collection |
NDLTD |
language |
English |
format |
Others
|
sources |
NDLTD |
topic |
Computer Sciences Datavetenskap (datalogi) |
spellingShingle |
Computer Sciences Datavetenskap (datalogi) Raabjerg, Palle Extending psi-calculi and their formal proofs |
description |
Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. This thesis presents broadcast psi-calculi and higher-order psi-calculi, two extensions of the psi-calculi framework, allowing respectively one-to-many communications and the use of higher-order process descriptions through conditions in the parameterised logic. Both extensions preserve the purity of the psi-calculi semantics; the standard congruence and structural properties of bisimilarity are proved formally in Isabelle. The work going into the extensions show that depending on the specific extension, working out the formal proofs can be a work-intensive process. We find that some of this work could be automated, and implementing such automation may facilitate the development of future extensions to the psi-calculi framework. === UPMARC |
author |
Raabjerg, Palle |
author_facet |
Raabjerg, Palle |
author_sort |
Raabjerg, Palle |
title |
Extending psi-calculi and their formal proofs |
title_short |
Extending psi-calculi and their formal proofs |
title_full |
Extending psi-calculi and their formal proofs |
title_fullStr |
Extending psi-calculi and their formal proofs |
title_full_unstemmed |
Extending psi-calculi and their formal proofs |
title_sort |
extending psi-calculi and their formal proofs |
publisher |
Uppsala universitet, Avdelningen för datalogi |
publishDate |
2012 |
url |
http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-183614 |
work_keys_str_mv |
AT raabjergpalle extendingpsicalculiandtheirformalproofs |
_version_ |
1718605013022932992 |