There is much prior and ongoing work that is related. Here we collect references to related stuff as we come accross it.
- “Generic Packet Descriptions: Verified Parsing and Pretty Printing of Low-Level Data” — Van Geest, Swierstra
- “NARCISSUS: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats” — Suriyakarn, Pit-Claudel, Delaware, Chlipala
- “A Scalable Module System” — Florian Rabe, Michael Kohlhase
- “Isomorphisms of finitary inductive types” — Kraus, Sattler
- Initial Algebra, Final Coalgebra and Datatype — Yeasin
- Initial Algebra Semantics is Enough! — Johann, Ghani
- Polynomial Functors and Polynomial Monads — Gambino, Kock
- Wikipedia: interface Description Language
- Wikipedia: comparison of data serialization formats
- dloss/binary-parsing: a nice compendium
- capnproto-flatbuffers (and flatbuffers definition language)
- Argdata: binary encoding
- Simple binary encoding
- Universal Binary Format
- cbor.io: Concise Binary Object Representation
- Cheerios: a verified de/serialization lib, part of the distributedcomponents.net project.
- generics-mrsop: Generic programming, with combinators, for mutually recursive families in the ‘sums of products’ style.
- Kaitai struct: a new way to develop parsers for binary structures.
- david-christiansen/b570abb9e7dabfe9074e: binary parsing in Idris, based on Power of Pi
- ION: jenkov.com
- scalaz/scalaz-schema and haskell-schema
- Katydid: regular expression based. supported native types
- Tenkei: Haskell tool for creating arbitrary language bindings
- Elm - types without borders ~ talk