Re: invertible protocol descriptions in Coq

[Anil Madhavapeddy <anil@xxxxxxxxxx>]

Right, but this is purely about the lexical/parsing problem, which is necessary 
(but not sufficient) to implement the whole protocol.  I believe Lem/Ott are 
more appropriate for specifying the dynamic semantic specification of how these 
'lexed' packets should be put together.

*Invertible* parsing is very useful though -- it covers the efficient 
construction of packets rather than just classification of incoming packets, 
and reduces code duplication.  This is what MPL solved, as well as Prashanth's 
follow up FP language [1], and the paper below.

[1] https://github.com/pmundkur/fp

-anil

On 18 Mar 2013, at 06:59, Jon Crowcroft <jon.crowcroft@xxxxxxxxxxxx> wrote:

> hm - so i think this is a weird paper - the example from eric rescorla's TLS 
> work is easily sorted with an LALR1 parser and tokenisning the input stream 
> not at the PACKET level, or byte, but by turning the protocol into a 
> collection of microprotocols- indeed, this is how most people think about TCP 
> - tcp is a collection of seperate protocols (state management for connection 
> setup/teardown; sequenced data delivery; flow control; congestion control' 
> urgent pointer; etc) living inside one packet format - don't get hung up on 
> the packet format - that is a mere _lexical_ problem...
> 
> On Sat, Mar 16, 2013 at 9:21 PM, Anil Madhavapeddy <anil@xxxxxxxxxx> wrote:
> 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
>