Extending psi-calculi and their formal proofs
2012 (English)Licentiate thesis, comprehensive summary (Other academic)
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.
Place, publisher, year, edition, pages
Uppsala universitet, 2012.
Information technology licentiate theses: Licentiate theses from the Department of Information Technology, ISSN 1404-5117 ; 2012-008
Research subject Computer Science
IdentifiersURN: urn:nbn:se:uu:diva-183614OAI: oai:DiVA.org:uu-183614DiVA: diva2:563554
2012-11-15, Room 1211, Polacksbacken, Lägerhyddsvägen 2, Uppsala, 10:15 (English)
Parrow, Joachim, ProfessorVictor, Björn, Docent
FunderSwedish Research Council
List of papers