2026-07-23T20:15:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13925 2024-03-06T10:53:09Z ddc:004 open_access

Specifying Message Formats with Contiguity Types Slind, Konrad Logic verification formal language theory message format languages We introduce Contiguity Types, a formalism for network message formats, aimed especially at self-describing formats. Contiguity types provide an intermediate layer between programming language data structures and messages, offering a helpful setting from which to automatically generate decoders, filters, and message generators. The syntax and semantics of contiguity types are defined and used to prove the correctness of a matching algorithm which has the flavour of a parser generator. The matcher has been used to enforce semantic well-formedness conditions on complex message formats for an autonomous unmanned avionics system. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Konrad Slind 2021 Is Part Of LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2021.30 urn:nbn:de:0030-drops-139252 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.30 eng https://creativecommons.org/licenses/by/4.0/legalcode