No Cover Image

Conference Paper/Proceeding/Abstract 546 views

Deriving pretty-big-step semantics from small-step semantics / Casper Bach Poulsen; Peter Mosses

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

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-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!
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 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.
Keywords: structural operational semantics, SOS, Modular SOS, pretty-big-step semantics, small-step semantics, big-step semantics, natural semantics, refocusing
College: College of Science
Start Page: 270
End Page: 289