Pretty-Big-Step Semantics

Abstract : In spite of the popularity of small-step semantics, big-step semantics remain used by many researchers. However, big-step semantics suffer from a serious duplication problem, which appears as soon as the semantics account for exceptions and/or divergence. In particular, many premises need to be copy-pasted across several evaluation rules. This duplication problem, which is particularly visible when scaling up to full-blown languages, results in formal definitions growing far bigger than necessary. Moreover, it leads to unsatisfactory redundancy in proofs. In this paper, we address the problem by introducing pretty-big-step semantics. Pretty-big-step semantics preserve the spirit of big-step semantics, in the sense that terms are directly related to their results, but they eliminate the duplication associated with big-step semantics.
Document type :
Conference papers
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/hal-00798227
Contributor : Arthur Charguéraud <>
Submitted on : Friday, March 8, 2013 - 11:09:42 AM
Last modification on : Friday, October 4, 2019 - 1:47:29 AM
Long-term archiving on : Sunday, April 2, 2017 - 10:19:40 AM

File

prettybigstep.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00798227, version 1

Collections

Citation

Arthur Charguéraud. Pretty-Big-Step Semantics. 22nd European Symposium on Programming (ESOP), Mar 2013, Rome, Italy. ⟨hal-00798227⟩

Share

Metrics

Record views

403

Files downloads

407