No Cover Image

Conference Paper/Proceeding/Abstract 1093 views

Modular bisimulation theory for computations and values

Martin Churchill, Peter Mosses Orcid Logo

FOSSACS: Foundations of Software Science and Computation Structures, Volume: 7794, Pages: 97 - 112

Swansea University Author: Peter Mosses Orcid Logo

Full text not available from this repository: check for access using links below.

Check full text

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

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><deptcode>FGSEN</deptcode><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><department>Science and Engineering - Faculty</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>FGSEN</DepartmentCode><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">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - 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 FGSEN 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 Science and Engineering - Faculty COLLEGE CODE FGSEN Swansea University 2015-04-22T13:30:10.9249176 2013-02-22T10:45:15.3085508 Faculty of Science and Engineering School of Mathematics and Computer 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 Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer 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:16:29Z
_version_ 1763750328848613376
score 11.037056

Similar Items