invertible protocol descriptions in Coq

[Anil Madhavapeddy <anil@xxxxxxxxxx>]

Found this very cool paper on specifying invertible protocol descriptions in 
Coq:

http://staff.aist.go.jp/reynald.affeldt/documents/plpv2012-preprint.pdf

..and they cover TLS.  It would be a nice project to extract this to 
OCaml/Haskell
to guarantee parsing equivalence from the formal spec (this is basically a much
better implementation of MPL or FP, embedded in the Coq proof assistant).

-anil