
A
Combinator
Library
for
PrefixFree
Codes
Title: 
A Combinator Library for PrefixFree Codes 
Author:

Emin Karayel

Submission date: 
20220408 
Abstract: 
This entry contains a set of binary encodings for primitive data
types, such as natural numbers, integers, floatingpoint 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 EliasGammaCodes and
exponential Golomb Codes, which are efficient variablelength codes in
use by current compression formats. A usecase for this library is
measuring the persisted size of a complex data structure without
having to handcraft a dedicated encoding for it, independent of
Isabelle's internal representation. 
BibTeX: 
@article{Prefix_Free_Code_CombinatorsAFP,
author = {Emin Karayel},
title = {A Combinator Library for PrefixFree Codes},
journal = {Archive of Formal Proofs},
month = apr,
year = 2022,
note = {\url{https://isaafp.org/entries/Prefix_Free_Code_Combinators.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Used by: 
Frequency_Moments 
