### Abstract

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.

### License

BSD License

### History

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)

### Topics

- Computer science/Data structures

### Session Native_Word

- Code_Target_Word_Base
- Word_Type_Copies
- Code_Int_Integer_Conversion
- Code_Target_Integer_Bit
- Uint64
- Uint32
- Uint16
- Uint8
- Uint
- Native_Cast
- Native_Cast_Uint
- Native_Word_Imperative_HOL
- Native_Word_Test
- Code_Target_Int_Bit
- Native_Word_Test_Emu
- Native_Word_Test_PolyML
- Native_Word_Test_PolyML2
- Native_Word_Test_PolyML64
- Native_Word_Test_Scala
- Native_Word_Test_GHC
- Native_Word_Test_MLton
- Native_Word_Test_MLton2
- Native_Word_Test_OCaml
- Native_Word_Test_OCaml2
- Native_Word_Test_SMLNJ
- Native_Word_Test_SMLNJ2
- Uint_Userguide

### Depends on

- Finite Machine Word Library

### Used by

- Verified Complete Test Strategies for Finite State Machines
- MiniSail - A kernel language for the ISA specification language SAIL
- Mersenne primes and the Lucas–Lehmer test
- WebAssembly
- Iptables Semantics
- Algorithms for Reduced Ordered Binary Decision Diagrams
- A Separation Logic Framework for Imperative HOL
- Generating linear orders for datatypes
- Collections Framework
- Jinja with Threads

### Auto-related entries

- Light-weight Containers
- A Verified Code Generator from Isabelle/HOL to CakeML
- XML
- Imperative Insertion Sort

## Cite

×

Native_Word-AFP

    @article{Native_Word-AFP,
      author  = {Andreas Lochbihler},
      title   = {Native Word},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Native_Word.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1