There is much prior and ongoing work that is related. Here we collect references to related stuff as we come accross it.


  1. “Generic Packet Descriptions: Verified Parsing and Pretty Printing of Low-Level Data” — Van Geest, Swierstra
  2. “NARCISSUS: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats” — Suriyakarn, Pit-Claudel, Delaware, Chlipala
  3. “A Scalable Module System” — Florian Rabe, Michael Kohlhase
  4. “Isomorphisms of finitary inductive types” — Kraus, Sattler
  5. Initial Algebra, Final Coalgebra and Datatype — Yeasin
  6. Initial Algebra Semantics is Enough! — Johann, Ghani
  7. Polynomial Functors and Polynomial Monads — Gambino, Kock

Related Projects