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
Relationally Staged Computations in Calculi of Mobile Processes
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Mobility)ORCID iD: 0000-0003-0174-9032
2004 (English)In: Proc. 7th Workshop on Coalgebraic Methods in Computer Science / [ed] J. Adámek, S. Milius, Elsevier , 2004, 105-120 p.Conference paper, Published paper (Refereed)
Abstract [en]

We apply the recently developed techniques of higher order abstract syntax and functorial operational semantics to give a compositional and fully abstract semantics for the π-calculus equipped with open bisimulation. The key novelty in our work is the realisation that the sophistication of open bisimulation requires us to move from the usual semantic domain of presheaves over subcategories of Set to presheaves over subcategories of Rel. This extra structure is crucial in controlling the renaming of extruded names and in providing a variety of different dynamic allocation operators to model the different binders of the π-calculus.

Place, publisher, year, edition, pages
Elsevier , 2004. 105-120 p.
Series
Electronic Notes in Theoretical Computer Science, ISSN 1571-0661 ; 106
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-93874DOI: 10.1016/j.entcs.2004.02.027OAI: oai:DiVA.org:uu-93874DiVA: diva2:167501
Conference
Workshop on Coalgebraic Methods in Computer Science (CMCS), Barcelona, Spain, 27–29 March 2004
Available from: 2005-12-22 Created: 2005-12-22 Last updated: 2016-02-25Bibliographically approved
In thesis
1. Relations in Models of Calculi and Logics with Names
Open this publication in new window or tab >>Relations in Models of Calculi and Logics with Names
2006 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

In this thesis we investigate two operational models of name-passing calculi: one based on coalgebra, and one based on enriched automata. We develop a semantic framework for modelling the open bisimulation in π-calculus, hyperbisimulation in Fusion calculus, and the first semantic interpretation of FOλ(nabla) logic.

We consider a category theoretic model where both “variables” and “names”, usually viewed as separate notions, are particular cases of the more general notion of atoms. The key aspect of this model is to consider functors over the category of irreflexive and symmetric finite relations. The models previously proposed for the separate notions of “variables” and “names” embed faithfully in the new one, and initial algebra/final coalgebra constructions can be transferred from the formers to the latter.

Moreover, the new model admits a definition of distinction-aware simultaneous substitutions. As a substantial application example, we give the first semantic interpretation of Miller-Tiu's FOλ(nabla) logic. FOλ(nabla) logic is designed for reasoning about operational semantics of languages with binding.

On the operational level, a contribution of the thesis is to extend an automata-based model for a variety of name-passing calculi with their associated notion of equivalence. HD-automata, a syntax-independent operational model, has been successfully applied for modelling e.g. early and late bisimulation in π-calculus and hyperbisimulation in Fusion calculus. However, current HD-automata are not adequate for modelling open bisimulation because they can not handle distinction-preserving substitutions. We solve this technical problem by integrating the notion of distinction into the definition of named sets, the basic building blocks of HD-automata. Finally, we discuss the relationship between HD-automata with distinctions, and D-LTS.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2006. viii + 128 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 132
Keyword
Process Calculi, Syntax, Semantics, HD-automata, Logic, Category theory
National Category
Computer Engineering
Identifiers
urn:nbn:se:uu:diva-6245 (URN)91-554-6426-2 (ISBN)
Public defence
2006-01-16, Room 1211, Polacksbacken, Lägerhyddsvägen 2F, Uppsala, 10:15 (English)
Opponent
Supervisors
Available from: 2005-12-22 Created: 2005-12-22 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Victor, Björn

Search in DiVA

By author/editor
Victor, Björn
By organisation
Computing Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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