A Combinator Library for Prefix-Free Codes (Q7361607)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Prefix_Free_Code_Combinators
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | A Combinator Library for Prefix-Free Codes |
AFP entry Prefix_Free_Code_Combinators |
Statements
8 April 2022
0 references
Emin Karayel
0 references
A Combinator Library for Prefix-Free Codes (English)
0 references
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.
0 references
