Pretty-Big-Step Semantics

Arthur Charguéraud 1, 2
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Type de document :
Communication dans un congrès
Matthias Felleisen and Philippa Gardner. 22nd European Symposium on Programming (ESOP), Mar 2013, Rome, Italy. Springer, 2013, Proceedings of the 22nd European Symposium on Programming
Liste complète des métadonnées


https://hal.inria.fr/hal-00798227
Contributeur : Arthur Charguéraud <>
Soumis le : vendredi 8 mars 2013 - 11:09:42
Dernière modification le : jeudi 9 février 2017 - 15:53:45
Document(s) archivé(s) le : dimanche 2 avril 2017 - 10:19:40

Fichier

prettybigstep.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00798227, version 1

Citation

Arthur Charguéraud. Pretty-Big-Step Semantics. Matthias Felleisen and Philippa Gardner. 22nd European Symposium on Programming (ESOP), Mar 2013, Rome, Italy. Springer, 2013, Proceedings of the 22nd European Symposium on Programming. <hal-00798227>

Partager

Métriques

Consultations de
la notice

274

Téléchargements du document

159