Skip to content

strict-types/strict-encoding

Strict encoding

Apache-2 licensed

Protobufs for functional programming

This is a set of libraries for deterministic binary serialization using strict types – type system made with category theory which ensures provable properties and bounds for the in-memory and serialized type representation.

The development of the libraries is performed by UBIDECO Institute.

Overview

Strict types is a formal notation for defining and serializing generalized algebraic data types (GADT) in a deterministic and confined way. It is developed with type theory in mind.

Strict Types are:

  • schema-based (with the schema being strict encoding notation),
  • semantic, i.e. defines types not just as they are layed out in memory, but also depending on their meaning,
  • deterministic, i.e. produces the same result for a given type,
  • portabile, i.e. can run on ahy hardware architecture and OS, including low-performant embedded systems,
  • confined, i.e. provides guarantees and static analysis on a maximum size of the typed data,
  • formally verifiable.

Strict Encoding is set of libraries for serializing / deserializing data types in binary formats.

strict-encoding-box

Libraries

Language Source code Package
Rust ./rust crates.io
Python Planned n/a
TypeScript Planned n/a
Swift Planned n/a
Kotlin Planned n/a

Contributing

CONTRIBUTING.md

License

The libraries are distributed on the terms of Apache 2.0 license.