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
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.