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 metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-01667321
Contributor : Hubert Garavel <>
Submitted on : Tuesday, December 19, 2017 - 11:46:17 AM
Last modification on : Saturday, December 15, 2018 - 1:49:36 AM

File

Garavel-17.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

996

Files downloads

328