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. 23rd International Workshop on Algebraic Development Techniques (WADT'2016), Sep 2017, Gregynog, Wales, UK, United Kingdom. Springer, Lecture Notes in Computer Science (10644), pp.120-134, 2017
Liste complète des métadonnées

Littérature citée [34 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 : jeudi 11 janvier 2018 - 06:23:43

Fichier

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

Identifiants

  • HAL Id : hal-01667321, version 1

Collections

Citation

Hubert Garavel. On the Most Suitable Axiomatization of Signed Integers. Phillip James; Markus Roggenbach. 23rd International Workshop on Algebraic Development Techniques (WADT'2016), Sep 2017, Gregynog, Wales, UK, United Kingdom. Springer, Lecture Notes in Computer Science (10644), pp.120-134, 2017. 〈hal-01667321〉

Partager

Métriques

Consultations de la notice

49

Téléchargements de fichiers

12