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. © 2014 Springer-Verlag.
CITATION STYLE
Bach Poulsen, C., & Mosses, P. D. (2014). Deriving pretty-big-step semantics from small-step semantics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8410 LNCS, pp. 270–289). Springer Verlag. https://doi.org/10.1007/978-3-642-54833-8_15
Mendeley helps you to discover research relevant for your work.