ASN.1 Floating Point encoding formalized in Coq
- High-level ASN.1 Real definition
- Conversion between ASN.1 and Flocq IEEE-754
- TODO: Bit-string encoding of ASN.1 real numbers
To install all pre-requisites:
opam repo add coq-released http://coq.inria.fr/opam/released
opam install coq coq-ext-lib coq-flocq coq-bbv dune num core coq-compcert
- Thanks to Sylvie Boldo and Guillaume Melquiond for their development of the Floats for Coq library, on which this project heavily relies both abstractly and with code.
- Thanks to Yury Strozhevsky for the great articles explaining the basics of ASN.1 encoding.
- Thanks to all the authors and contributors of the StructTact library.