A typed model for encoding-based protocol interoperability

Documentation of the HTTP protocol includes precise descriptions of the syntax of the protocol, but lacks similarly precise specification of the semantics of messages and message bodies. Semantics are stated in English prose; while this makes the document more intuitively accessible, it makes any sort of formal claims of correctness or interoperability difficult to derive from the specification itself. We propose "layered types", a formal description of the interpretive semantics of HTTP message bodies based upon the stacked type syntax. This model allows us to formally declare semantics for content-related HTTP headers and offers a precise way of characterizing interoperability between current and future protocol revisions and extensions.