cheerios
Serialization library
A formally verified serialization library for Coq
Formally verified Coq serialization library with support for extraction to OCaml
23 stars
30 watching
5 forks
Language: Coq
last commit: about 1 year ago coqcoq-libraryocamlproofserializationserialization-library
Related projects:
| Repository | Description | Stars |
|---|---|---|
| uwplse/pumpkin-pi | Automatically discovers and proves relationships between types in Coq to simplify proof development and code reuse. | 49 |
| uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 imdea-software/fcsl-pcm | Provides formalisation of Partial Commutative Monoids (PCMs) for verification of pointer-manipulating sequential and concurrent programs. | 26 |
| ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 coq-concurrency/pluto | A Coq-based web server written in a functional programming language | 86 |
 coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 uds-psl/coq-library-undecidability | A collection of mechanized undecidability proofs in Coq | 111 |
 snu-sf/paco | A Coq library for proving properties about stateful systems through parameterized coinduction | 43 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 354 |
 weebly/cereal | A Swift serialization framework allowing encoding and decoding of various data types | 369 |
 jacob-carlborg/orange | A serialization library for the D programming language. | 72 |
 nixman/yas | An efficient serialization library with support for various data types and formats | 732 |
 lysxia/coq-simple-io | Provides tools to implement IO programs directly in Coq | 31 |