Projects per year
Abstract
We investigate operational and denotational semantics for computational and concurrent systems with mobile names which capture their computational properties. For example, various properties of fixed networks, such as shortest or longest path, transition probabilities, and secure data flows, correspond to the "sum" in a semiring of the weights of paths through the network: we aim to model networks with a dynamic topology in a similar way. Alongside rich computational formalisms such as the λ-calculus, these can be represented as terms in a calculus of solos with weights from a complete semiring R, so that reduction associates a weight in R to each reduction path. Taking inspiration from differential nets, we develop a denotational semantics for this calculus in the category of sets and R-weighted relations, based on its differential and compact-closed structure, but giving a simple, syntax-independent representation of terms as matrices over R. We show that this corresponds to the sum in R of the values associated to its independent reduction paths, and that our semantics is fully abstract with respect to the observational equivalence induced by sum-of-paths evaluation.
Original language | English |
---|---|
Title of host publication | Leibniz International Proceedings in Informatics, LIPIcs |
Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
Pages | 1-15 |
Number of pages | 15 |
Volume | 52 |
ISBN (Print) | 9783959770101 |
DOIs | |
Publication status | Published - 1 Jun 2016 |
Event | 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 - Porto, Portugal Duration: 22 Jun 2016 → 26 Jun 2016 |
Conference
Conference | 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016 |
---|---|
Country/Territory | Portugal |
City | Porto |
Period | 22/06/16 → 26/06/16 |
Keywords
- Concurrency
- Mobility
- Solos
ASJC Scopus subject areas
- Software
Fingerprint
Dive into the research topics of 'Weighted relational models for mobility'. Together they form a unique fingerprint.Projects
- 2 Finished
-
Semantic Types for Verified Program Behaviour
Laird, J. (PI)
Engineering and Physical Sciences Research Council
28/02/14 → 31/07/17
Project: Research council
-
Semantic Structures for Higher-Order Information Flow
Laird, J. (PI)
Engineering and Physical Sciences Research Council
20/06/10 → 19/06/12
Project: Research council