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

### License

BSD License

### Topics

- Computer science/Algorithms
- Computer science/Data structures

### Session Prefix_Free_Code_Combinators

- Prefix_Free_Code_Combinators
- Examples

### Used by

- Formalization of Randomized Approximation Algorithms for Frequency Moments

## Cite

×

Prefix_Free_Code_Combinators-AFP

    @article{Prefix_Free_Code_Combinators-AFP,
      author  = {Emin Karayel},
      title   = {A Combinator Library for Prefix-Free Codes},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Prefix_Free_Code_Combinators.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Apr 19, 2022 : Isabelle2021-1