No Cover Image

Conference Paper/Proceeding/Abstract 973 views

Deriving pretty-big-step semantics from small-step semantics

Casper Bach Poulsen, Peter Mosses Orcid Logo

Programming Languages and Systems, Volume: 8410, Pages: 270 - 289

Swansea University Author: Peter Mosses Orcid Logo

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

DOI (Published version): 10.1007/978-3-642-54833-8_15

Abstract

Big-step semantics for languages with abrupt termination and/or divergence suffer from a serious duplication problem, addressed by the novel ‘pretty-big-step’ style presented by Charguéraud at ESOP’13. Such rules are less concise than corresponding small-step rules, but they have the same advantages...

Full description

Published in: Programming Languages and Systems
Published: Berlin Heidelberg Springer 2014
URI: https://cronfa.swan.ac.uk/Record/cronfa17526
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2014-03-25T02:30:09Z
last_indexed 2019-02-11T19:06:18Z
id cronfa17526
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-02-11T15:51:26.4244661</datestamp><bib-version>v2</bib-version><id>17526</id><entry>2014-03-24</entry><title>Deriving pretty-big-step semantics from small-step semantics</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>2014-03-24</date><deptcode>FGSEN</deptcode><abstract>Big-step semantics for languages with abrupt termination and/or divergence suffer from a serious duplication problem, addressed by the novel &#x2018;pretty-big-step&#x2019; style presented by Chargu&#xE9;raud at ESOP&#x2019;13. Such rules are less concise than corresponding small-step rules, but they have the same advantages as big-step rules for program correctness proofs. Here, we show how to automatically derive pretty-big-step rules directly from small-step rules by &#x2018;refocusing&#x2019;. This gives the best of both worlds: we only need to write the relatively concise small-step specifications, but our reasoning can be big-step as well as small-step. The use of strictness annotations to derive small-step congruence rules gives further conciseness.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Programming Languages and Systems</journal><volume>8410</volume><paginationStart>270</paginationStart><paginationEnd>289</paginationEnd><publisher>Springer</publisher><placeOfPublication>Berlin Heidelberg</placeOfPublication><keywords>structural operational semantics, SOS, Modular SOS, pretty-big-step semantics, small-step semantics, big-step semantics, natural semantics, refocusing</keywords><publishedDay>31</publishedDay><publishedMonth>3</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-03-31</publishedDate><doi>10.1007/978-3-642-54833-8_15</doi><url/><notes/><college>COLLEGE NANME</college><department>Science and Engineering - Faculty</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>FGSEN</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2019-02-11T15:51:26.4244661</lastEdited><Created>2014-03-24T09:48:59.4967666</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>Casper</firstname><surname>Bach Poulsen</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 2019-02-11T15:51:26.4244661 v2 17526 2014-03-24 Deriving pretty-big-step semantics from small-step semantics 3f13b8ec315845c81d371f41e772399c 0000-0002-5826-7520 Peter Mosses Peter Mosses true false 2014-03-24 FGSEN Big-step semantics for languages with abrupt termination and/or divergence suffer from a serious duplication problem, addressed by the novel ‘pretty-big-step’ style presented by Charguéraud at ESOP’13. Such rules are less concise than corresponding small-step rules, but they have the same advantages as big-step rules for program correctness proofs. Here, we show how to automatically derive pretty-big-step rules directly from small-step rules by ‘refocusing’. This gives the best of both worlds: we only need to write the relatively concise small-step specifications, but our reasoning can be big-step as well as small-step. The use of strictness annotations to derive small-step congruence rules gives further conciseness. Conference Paper/Proceeding/Abstract Programming Languages and Systems 8410 270 289 Springer Berlin Heidelberg structural operational semantics, SOS, Modular SOS, pretty-big-step semantics, small-step semantics, big-step semantics, natural semantics, refocusing 31 3 2014 2014-03-31 10.1007/978-3-642-54833-8_15 COLLEGE NANME Science and Engineering - Faculty COLLEGE CODE FGSEN Swansea University 2019-02-11T15:51:26.4244661 2014-03-24T09:48:59.4967666 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Casper Bach Poulsen 1 Peter Mosses 0000-0002-5826-7520 2
title Deriving pretty-big-step semantics from small-step semantics
spellingShingle Deriving pretty-big-step semantics from small-step semantics
Peter Mosses
title_short Deriving pretty-big-step semantics from small-step semantics
title_full Deriving pretty-big-step semantics from small-step semantics
title_fullStr Deriving pretty-big-step semantics from small-step semantics
title_full_unstemmed Deriving pretty-big-step semantics from small-step semantics
title_sort Deriving pretty-big-step semantics from small-step semantics
author_id_str_mv 3f13b8ec315845c81d371f41e772399c
author_id_fullname_str_mv 3f13b8ec315845c81d371f41e772399c_***_Peter Mosses
author Peter Mosses
author2 Casper Bach Poulsen
Peter Mosses
format Conference Paper/Proceeding/Abstract
container_title Programming Languages and Systems
container_volume 8410
container_start_page 270
publishDate 2014
institution Swansea University
doi_str_mv 10.1007/978-3-642-54833-8_15
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
document_store_str 0
active_str 0
description Big-step semantics for languages with abrupt termination and/or divergence suffer from a serious duplication problem, addressed by the novel ‘pretty-big-step’ style presented by Charguéraud at ESOP’13. Such rules are less concise than corresponding small-step rules, but they have the same advantages as big-step rules for program correctness proofs. Here, we show how to automatically derive pretty-big-step rules directly from small-step rules by ‘refocusing’. This gives the best of both worlds: we only need to write the relatively concise small-step specifications, but our reasoning can be big-step as well as small-step. The use of strictness annotations to derive small-step congruence rules gives further conciseness.
published_date 2014-03-31T03:20:15Z
_version_ 1763750565792186368
score 11.016235

Similar Items