%0 Conference Proceedings
%T On the Most Suitable Axiomatization of Signed Integers
%+ Construction of verified concurrent systems (CONVECS )
%+ Universität des Saarlandes [Saarbrücken]
%A Garavel, Hubert
%Z Part 4: Regular Papers
%< avec comité de lecture
%Z work done under the aegis of the Alexander-von-Humboldt foundation
%( Lecture Notes in Computer Science
%B 23th International Workshop on Algebraic Development Techniques (WADT)
%C Gregynog, Wales, UK, United Kingdom
%Y Phillip James
%Y Markus Roggenbach
%I Springer
%3 Recent Trends in Algebraic Development Techniques
%V LNCS-10644
%N 10644
%P 120-134
%8 2017-09-21
%D 2017
%R 10.1007/978-3-319-72044-9_9
%K natural number
%K theorem proving
%K number theory
%K term rewrite system
%K formal method
%K algebraic specification
%K abstract data type
%K computer language
%K integer number
%K semantics
%Z Computer Science [cs]/Discrete Mathematics [cs.DM]
%Z Computer Science [cs]/Symbolic Computation [cs.SC]Conference papers
%X 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.
%G English
%Z TC1
%Z WG1.3
%2 https://inria.hal.science/hal-01667321/document
%2 https://inria.hal.science/hal-01667321/file/Garavel-17.pdf
%L hal-01667321
%U https://inria.hal.science/hal-01667321
%~ UNIV-RENNES1
%~ UGA
%~ CNRS
%~ INRIA
%~ INPG
%~ INRIA-RHA
%~ IRISA
%~ LIG
%~ OPENAIRE
%~ INRIA_TEST
%~ LIG_MFML_CONVECS
%~ CONVECS
%~ TESTALAIN1
%~ IFIP-LNCS
%~ IFIP
%~ INRIA2
%~ IFIP-TC
%~ IFIP-TC1
%~ TDS-MACS
%~ UR1-HAL
%~ UR1-MATH-STIC
%~ IFIP-WG1-3
%~ UR1-UFR-ISTIC
%~ IFIP-WADT
%~ INRIA2017
%~ TEST-UR-CSS
%~ UNIV-RENNES
%~ INRIA-RENGRE
%~ IFIP-LNCS-10644
%~ INRIA-300009
%~ UGA-COMUE
%~ UR1-MATH-NUM
%~ LIG_SIDCH
%~ INRIA-ALLEMAGNE