Native Word

Andreas Lochbihler 🌐 with contributions from Peter Lammich 🌐

September 17, 2013

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This entry makes machine words and machine arithmetic available for code generation from Isabelle/HOL. It provides a common abstraction that hides the differences between the different target languages. The code generator maps these operations to the APIs of the target languages. Apart from that, we extend the available bit operations on types int and integer, and map them to the operations in the target languages.


BSD License


July 15, 2018
added cast operators for default-size words (revision fc1f1fb8dd30)
September 2, 2017
added 64-bit words (revision c89f86244e3c)
October 6, 2014
proper test setup with compilation and execution of tests in all target languages (revision 5d7a1c9ae047)
March 31, 2014
added words of default size in the target language (by Peter Lammich) (revision 25caf5065833)
November 6, 2013
added conversion function between native words and characters (revision fd23d9a7fe3a)


Session Native_Word