| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
A Combinator Library for Prefix-Free Codes
| Title: | A Combinator Library for Prefix-Free Codes |
| Author: | Emin Karayel |
| Submission date: | 2022-04-08 |
| Abstract: | This entry contains a set of binary encodings for primitive data types, such as natural numbers, integers, floating-point numbers as well as combinators to construct encodings for products, lists, sets or functions of/between such types. For natural numbers and integers, the entry contains various encodings, such as Elias-Gamma-Codes and exponential Golomb Codes, which are efficient variable-length codes in use by current compression formats. A use-case for this library is measuring the persisted size of a complex data structure without having to hand-craft a dedicated encoding for it, independent of Isabelle's internal representation. |
| BibTeX: |
@article{Prefix_Free_Code_Combinators-AFP,
author = {Emin Karayel},
title = {A Combinator Library for Prefix-Free Codes},
journal = {Archive of Formal Proofs},
month = apr,
year = 2022,
note = {\url{https://isa-afp.org/entries/Prefix_Free_Code_Combinators.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Used by: | Frequency_Moments |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
| Older releases: None |