| TRX: A Formally Verified Parser Interpreter |  |
Abstract:
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.
TRX: A Formally Verified Parser Interpreter
In
Logical Methods in Computer Science (LMCS),
7(2),
2011.
BibTeX:@article{trx-LMCS-11,
author = {Adam Koprowski and Henri Binsztok},
title = {{TRX}: A Formally Verified Parser Interpreter},
journal = {Logical Methods in Computer Science (LMCS)},
year = {2011},
volume = {7},
number = {2},
pages = {},
} | 
