Conference Paper/Proceeding/Abstract 973 views
Deriving pretty-big-step semantics from small-step semantics
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...
| 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: |
Faculty of Science and Engineering |
| Start Page: |
270 |
| End Page: |
289 |