TRX: A Formally Verified Parser Interpreter

TL;DR

This paper introduces TRX, a parser interpreter developed in Coq that guarantees total correctness and termination for PEG-based parsers, offering a formally verified solution to parsing.

Contribution

It presents the first formal verification of a PEG parser interpreter in Coq, ensuring correctness and termination.

Findings

Parser produced is formally correct and terminating.

Formal proofs of correctness and termination in Coq.

Applicable to arbitrary PEG grammars.

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.