zbMATH — the first resource for mathematics

TRX: a formally verified parser interpreter. (English) Zbl 1260.68194
Gordon, Andrew D. (ed.), Programming languages and systems. 19th European symposium on programming, ESOP 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-11956-9/pbk). Lecture Notes in Computer Science 6012, 345-365 (2010).
Summary: Parsing is an important problem in computer science and yet surprisingly little attention has been devoted to its formal verification. In this paper, we present TRX: a parser interpreter formally developed in the proof assistant Coq, capable of producing formally correct parsers. We are using parsing expression grammars (PEGs), a formalism essentially representing recursive descent parsing, which we consider an attractive alternative to context-free grammars (CFGs). From this formalization we can extract a parser for an arbitrary PEG grammar with the warranty of total correctness, i.e., the resulting parser is terminating and correct with respect to its grammar and the semantics of PEGs; both properties formally proven in Coq.
For the entire collection see [Zbl 1182.68003].

68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
CompCert; Coq; TRX
Full Text: DOI