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
A unifying model of variables and names
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Mobility)
2004 (English)Report (Other academic)
Place, publisher, year, edition, pages
Department of Mathematics and Computer Science, University of Udine , 2004.
Series
Research Report UDMI, 15/2004/RR
Identifiers
URN: urn:nbn:se:uu:diva-93875OAI: oai:DiVA.org:uu-93875DiVA: diva2:167502
Available from: 2005-12-22 Created: 2005-12-22 Last updated: 2009-11-30Bibliographically 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

By organisation
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

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