On the Most Suitable Axiomatization of Signed Integers

Hubert Garavel

Post-proceedings (December 2017) of the 23rd International Workshop on Algebraic Development Techniques (WADT'16), Gregynog, Wales, UK, September 2016

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.

16 pages

PDF

PostScript

(Revised) slides of H. Garavel's lecture at the WADT'16 workshop

PDF