On the Most Suitable Axiomatization of Signed Integers

Hubert Garavel 1, 2
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : The standard mathematical definition of signed integers, based on set theory, is not well-adapted to the needs of computer science. For this reason, many formal specification languages and theorem provers have designed alternative definitions of signed integers based on term algebras , by extending the Peano-style construction of unsigned naturals using "zero" and "succ" to the case of signed integers. We compare the various approaches used in CADP, CASL, Coq, Isabelle/HOL, KIV, Maude, mCRL2, PSF, SMT-LIB, TLA+, etc. according to objective criteria and suggest an "optimal" definition of signed integers.
Type de document :
Communication dans un congrès
Phillip James; Markus Roggenbach. 23th International Workshop on Algebraic Development Techniques (WADT), Sep 2017, Gregynog, Wales, UK, United Kingdom. Springer, Lecture Notes in Computer Science, LNCS-10644 (10644), pp.120-134, 2017, Recent Trends in Algebraic Development Techniques. 〈10.1007/978-3-319-72044-9_9 〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01667321
Contributeur : Hubert Garavel <>
Soumis le : mardi 19 décembre 2017 - 11:46:17
Dernière modification le : samedi 15 décembre 2018 - 01:49:36

Fichier

Garavel-17.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Hubert Garavel. On the Most Suitable Axiomatization of Signed Integers. Phillip James; Markus Roggenbach. 23th International Workshop on Algebraic Development Techniques (WADT), Sep 2017, Gregynog, Wales, UK, United Kingdom. Springer, Lecture Notes in Computer Science, LNCS-10644 (10644), pp.120-134, 2017, Recent Trends in Algebraic Development Techniques. 〈10.1007/978-3-319-72044-9_9 〉. 〈hal-01667321〉

Partager

Métriques

Consultations de la notice

701

Téléchargements de fichiers

116