The End of History? Using a Proof Assistant to Replace Language Design with Library Design. - Adam Chlipala; Benjamin Delaware; Samuel Duchovni; Jason Gross; Clément Pit-Claudel; Sorawit Suriyakarn; Peng Wang 048; Katherine Ye (SNAPL, 2017)

Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. - Sorawit Suriyakarn; Clément Pit-Claudel; Benjamin Delaware; Adam Chlipala (CoRR, 2018)

Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. - Benjamin Delaware; Sorawit Suriyakarn; Clément Pit-Claudel; Qianchuan Ye; Adam Chlipala (Proc. ACM Program. Lang., 2019)