No Cover Image

Conference Paper/Proceeding/Abstract 557 views

Modular bisimulation theory for computations and values / Martin Churchill; Peter Mosses

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.

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...

Full description

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!
first_indexed 2013-07-23T12:12:07Z
last_indexed 2018-02-09T04:45:44Z
id cronfa14363
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2015-04-22T13:30:10.9249176</datestamp><bib-version>v2</bib-version><id>14363</id><entry>2013-02-22</entry><title>Modular bisimulation theory for computations and values</title><swanseaauthors><author><sid>3f13b8ec315845c81d371f41e772399c</sid><ORCID>0000-0002-5826-7520</ORCID><firstname>Peter</firstname><surname>Mosses</surname><name>Peter Mosses</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2013-02-22</date><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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>FOSSACS: Foundations of Software Science and Computation Structures</journal><volume>7794</volume><paginationStart>97</paginationStart><paginationEnd>112</paginationEnd><publisher>Springer</publisher><placeOfPublication>Berlin</placeOfPublication><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords/><publishedDay>28</publishedDay><publishedMonth>2</publishedMonth><publishedYear>2013</publishedYear><publishedDate>2013-02-28</publishedDate><doi>10.1007/978-3-642-37075-5_7</doi><url>http://link.springer.com/chapter/10.1007%2F978-3-642-37075-5_7</url><notes>Lecture Notes in Computer Science</notes><college>COLLEGE NANME</college><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><apcterm/><lastEdited>2015-04-22T13:30:10.9249176</lastEdited><Created>2013-02-22T10:45:15.3085508</Created><path><level id="1">College of Science</level><level id="2">Computer Science</level></path><authors><author><firstname>Martin</firstname><surname>Churchill</surname><order>1</order></author><author><firstname>Peter</firstname><surname>Mosses</surname><orcid>0000-0002-5826-7520</orcid><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2015-04-22T13:30:10.9249176 v2 14363 2013-02-22 Modular bisimulation theory for computations and values 3f13b8ec315845c81d371f41e772399c 0000-0002-5826-7520 Peter Mosses Peter Mosses true false 2013-02-22 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. Conference Paper/Proceeding/Abstract FOSSACS: Foundations of Software Science and Computation Structures 7794 97 112 Springer Berlin 0302-9743 1611-3349 28 2 2013 2013-02-28 10.1007/978-3-642-37075-5_7 http://link.springer.com/chapter/10.1007%2F978-3-642-37075-5_7 Lecture Notes in Computer Science COLLEGE NANME COLLEGE CODE Swansea University 2015-04-22T13:30:10.9249176 2013-02-22T10:45:15.3085508 College of Science Computer Science Martin Churchill 1 Peter Mosses 0000-0002-5826-7520 2
title Modular bisimulation theory for computations and values
spellingShingle Modular bisimulation theory for computations and values
Peter, Mosses
title_short Modular bisimulation theory for computations and values
title_full Modular bisimulation theory for computations and values
title_fullStr Modular bisimulation theory for computations and values
title_full_unstemmed Modular bisimulation theory for computations and values
title_sort Modular bisimulation theory for computations and values
author_id_str_mv 3f13b8ec315845c81d371f41e772399c
author_id_fullname_str_mv 3f13b8ec315845c81d371f41e772399c_***_Peter, Mosses
author Peter, Mosses
author2 Martin Churchill
Peter Mosses
format Conference Paper/Proceeding/Abstract
container_title FOSSACS: Foundations of Software Science and Computation Structures
container_volume 7794
container_start_page 97
publishDate 2013
institution Swansea University
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-642-37075-5_7
publisher Springer
college_str College of Science
hierarchytype
hierarchy_top_id collegeofscience
hierarchy_top_title College of Science
hierarchy_parent_id collegeofscience
hierarchy_parent_title College of Science
department_str Computer Science{{{_:::_}}}College of Science{{{_:::_}}}Computer Science
url http://link.springer.com/chapter/10.1007%2F978-3-642-37075-5_7
document_store_str 0
active_str 0
description 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.
published_date 2013-02-28T03:26:30Z
_version_ 1702688604284780544
score 10.801427