| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Native Word
| Title: | Native Word |
| Author: | Andreas Lochbihler |
| Contributor: | Peter Lammich |
| Submission date: | 2013-09-17 |
| 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. |
| Change history: | [2013-11-06]:
added conversion function between native words and characters
(revision fd23d9a7fe3a) [2014-03-31]: added words of default size in the target language (by Peter Lammich) (revision 25caf5065833) [2014-10-06]: proper test setup with compilation and execution of tests in all target languages (revision 5d7a1c9ae047) [2017-09-02]: added 64-bit words (revision c89f86244e3c) [2018-07-15]: added cast operators for default-size words (revision fc1f1fb8dd30) |
| BibTeX: |
@article{Native_Word-AFP,
author = {Andreas Lochbihler},
title = {Native Word},
journal = {Archive of Formal Proofs},
month = sep,
year = 2013,
note = {\url{http://isa-afp.org/entries/Native_Word.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Used by: | Collections, Datatype_Order_Generator, Iptables_Semantics, JinjaThreads, ROBDD, Separation_Logic_Imperative_HOL, WebAssembly |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |