some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

   Volume 3 (2007)

   Volume 4 (2008)

   Volume 5 (2009)

   Volume 6 (2010)

   Volume 7 (2011)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

   Volume 8 (2012)

   Volume 9 (2013)

   Volume 10 (2014)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

VOLUME 7, ISSUE 2, PAPER 18


TRX: A Formally Verified Parser Interpreter

©Adam Koprowski, MLstate, Paris, France
©Henri Binsztok, MLstate, Paris, France

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.

Publication date: June 24, 2011

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-7(2:18)2011

Hit Counts: 4408

Creative Commons