Bells and Whistles: Advanced language features in psi-calculi
2013 (English)Licentiate thesis, comprehensive summary (Other academic)
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 universitet, 2013.
Information technology licentiate theses: Licentiate theses from the Department of Information Technology, ISSN 1404-5117 ; 2013-004
Research subject Computer Science
IdentifiersURN: urn:nbn:se:uu:diva-227638OAI: oai:DiVA.org:uu-227638DiVA: diva2:730682
Parrow, Joachim, ProfessorVictor, Björn, Docent
List of papers