Skip to Main content Skip to Navigation
New interface
Conference papers

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.
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Hubert Garavel Connect in order to contact the contributor
Submitted on : Tuesday, December 19, 2017 - 11:46:17 AM
Last modification on : Monday, July 25, 2022 - 3:44:38 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Hubert Garavel. On the Most Suitable Axiomatization of Signed Integers. 23th International Workshop on Algebraic Development Techniques (WADT), Sep 2017, Gregynog, Wales, UK, United Kingdom. pp.120-134, ⟨10.1007/978-3-319-72044-9_9⟩. ⟨hal-01667321⟩



Record views


Files downloads