Conference Paper/Proceeding/Abstract 1093 views
Modular bisimulation theory for computations and values
FOSSACS: Foundations of Software Science and Computation Structures, Volume: 7794, Pages: 97 - 112
Swansea University Author:
Peter Mosses
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1007/978-3-642-37075-5_7
Abstract
For structural operational semantics (SOS) of process algebras, various notions of bisimulation have been studied, together with rule formats ensuring that bisimilarity is a congruence. For programming languages, however, SOS generally involves auxiliary entities (e.g. stores) and computed values, a...
| Published in: | FOSSACS: Foundations of Software Science and Computation Structures |
|---|---|
| ISSN: | 0302-9743 1611-3349 |
| Published: |
Berlin
Springer
2013
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa14363 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
For structural operational semantics (SOS) of process algebras, various notions of bisimulation have been studied, together with rule formats ensuring that bisimilarity is a congruence. For programming languages, however, SOS generally involves auxiliary entities (e.g. stores) and computed values, and the standard bisimulation and rule formats are not directly applicable.Here, we first introduce a notion of bisimulation based on the distinction between computations and values, with a corresponding liberal congruence format. We then provide metatheory for a modular variant of SOS (MSOS) which provides a systematic treatment of auxiliary entities. This is based on a higher order form of bisimulation, and we formulate an appropriate congruence format. Finally, we show how algebraic laws can be proved sound for bisimulation with reference only to the (M)SOS rules defining the programming constructs involved in them. Such laws remain sound for languages that involve further constructs. |
|---|---|
| Item Description: |
Lecture Notes in Computer Science |
| College: |
Faculty of Science and Engineering |
| Start Page: |
97 |
| End Page: |
112 |